alt Hacker NewsAsk the model to declare its assumed axioms. Agree that those can be trusted for the time being. Things like the behaviour of third party libraries. Ensure that your review agent enforces this.
Ask the model to declare its assumed axioms. Agree that those can be trusted for the time being. Things like the behaviour of third party libraries. Ensure that your review agent enforces this.
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.