x.com/perrymetzger/status/2042575263666471057

This claim is too strong because it says these techniques require AI to be usable in practice. Credible, pre-LLM examples show the opposite: human researchers and engineers have been using formal verification on production-relevant software for many years.

• The seL4 project states that its kernel has a "formal mathematical proof" and that those machine-checked proofs imply the absence of whole classes of bugs such as buffer overflows and memory leaks. That is a long-running, real-world formal verification effort, not something that depended on modern AI.
• The official CompCert site describes CompCert C as a compiler that is "formally verified, using machine-assisted mathematical proofs" and notes public releases going back to 2008. That directly contradicts the idea that humans could not meaningfully take advantage of formal verification before AI.
• AWS described adding automated formal verification to its s2n TLS library in 2016, explaining that formal verification is typically done by "skilled specialists using mathematical toolsets" and that AWS used a toolchain from Galois to verify parts of s2n. Again, this is a practical use of formal verification years before current AI coding systems.

A narrower claim like "AI may make formal verification cheaper or more scalable" would be arguable. But the posted wording says formal verification techniques require AI because they are too labor-intensive for humans, and the existence of major human-driven formal verification projects shows that is incorrect.