I feel like leaving it to decide everything would not produce a good end product. It feels like just having it decide how GC should work, how the function call stack should work or any of these rather simple but actually requiring lots of decision and thinking how things fit together (and pick a good solution out of many seemingly good solutions that can come back to bite you), couple this with the tendency for AI agents to tend towards adding new code and building over features I don't think you end up with a good solution.

On formal verification having done it only in an academic sense and looked over at projects like seL4 and quite interested in that project. It feels like actually proving useful properties of programs for real programs even ones with well defined domains and easier to model such as interpreters or compilers it seems that it will just prove theorems about properties that hardly matter or don't even matter at all. See how bad it still tends to be when trying to get it to write tests.

I would be interested to know if their has been an agent that has actually utilized formal methods such as Lean or Coq or Isabella to prove properties of programs in an automated way as you suggest, I have only seen it proving mathematics and or searching for counter examples, not writing Curry-Howard style proofs.