I think incompleteness theorem means that you can't guarantee the agents will always be able to converge on a proof, since you can't have both completeness and soundness (and we obviously need soundness since that's the whole point of a theorem prover).

But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).

And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)

> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.

> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.

That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".

> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."

I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.