Formal Verification Is Back: 50-Year-Old Arguments Against It, Revisited

The Case Against Formal Verification, 50 Years Later

Formal verification is suddenly hot, driven by AI coding agents that need correctness guarantees. This post revisits the classic 1979 paper 'Social Processes and Proofs of Theorems and Programs,' which argued verification would fail. The author examines each argument in light of modern developments—LLM-powered proof assistants, interactive specification tools, and the rise of AI agents—concluding that while full verification isn't a silver bullet, formal methods are more valuable than ever for specifying intent and closing the loop on AI-generated code.