My issue with formal proofs for code is that it assumes that the code is static and requirements are fixed and won't change. This assumption doesn't hold up in the vast majority of projects.
Surely LLMs can make this more practical but I think many projects suffer from a more mundane problem that they aren't architected properly. Without proper separation of concerns and proper abstraction, you won't get stability in the base modules, which means that you will have to re-evaluate and re-write tests and formal proofs constantly.
This issue seems hallucinated. In the real world we just update our proofs. https://sos-vo.org/node/69931
How hypocritical of someone preaching the virtues of formal proofs to be using a single example to try to prove the 'for all' case... As if it's feasible for all systems, for all requirements, under all possible financial constraints.
Oh yes, I'm the LLM here.
Maybe you should run your comments through your Coq proof-assistant before you post them!