Thanks for the advice. This is what I struggle with the most. I’ve learned formal verification other than Lean proofs and used it a few times. It holds up well, but as soon as it becomes a slightly longer-term task, it passes formal verification but turns into work that doesn’t reach the goal G I’m aiming for, and I don’t know how to solve that. I clearly need a separate review agent—have you built a separate harness for the review agent?

Other people say that when they do AI coding, they finish quickly, but for me it’s painful because I keep having to verify it myself.