Revisiting 'The Case Against Formal Verification' 50 Years Later in the Age of AI Coding

The Case Against Formal Verification, 50 Years Later

Ivan Gavran revisits the 1979 paper that argued formal verification was bound to fail, checking each claim against today's AI coding landscape. The original said fully automatic verifiers were unlikely; LLM-powered tools are now closing that gap, with Igor Konnov proving the Ben-Or protocol's safety in Lean as one example. The worry about spec-implementation contamination gets flipped: with coding agents in the loop, humans become the clearer final arbiter of correctness. Gavran concedes the original point that messy real-world systems often aren't worth verifying still holds. His overall take is measured: interest is spiking, but mainstream adoption isn't here yet.

Why it matters: A blog post with a clear argument, concrete examples, and historical context — not marketing fluff. Hits all three HKR axes, but as a personal blog it lacks institutional weight, so default to the lower band at 72.