I agree with this to some degree. Agents often stub and take shortcuts during implementation. I've been working on this problem a little bit with open-artisan which I published yesterday (https://github.com/yehudacohen/open-artisan).

Rather than having agents decide to manage their own code lifecycle, define a state machine where code moves from agent to agent and isolated agents critique each others code until the code produced is excellent quality.

This is still a bit of an token hungry solution, but it seems to be working reasonably well so far and I'm actively refining it as I build.

Not going to give you formal verification, but might be worth looking into strategies like this.