The Case Against Formal Verification, 50 Years Later

Join the discussion

• Hacker News
• I agree that a correctness proof for a complete, large program will always have the problem that the specification itself might be buggy. So integration tests will hardly ever become unnecessary. But as others have already pointed out, even then formal verification of critical parts of a program can be useful. I would like to add that it can also be of great value if one can "only" prove that a program will never trigger undefined behaviour, or cause a runtime error. For C programs, that would, of course, be particularly helpful. But even in safe Rust, there can be (in my understanding, I haven't yet used Rust myself) runtime errors in the form of panics. And if your medical device stops working, because the software attempted an out-of-bounds read or write and was therefore aborted with a panic, that isn't really fun. Better to prove statically that such invalid accesses will never occur. And this is still for safe Rust - not even considering unsafe code. Similar arguments hold for other system-level programming languages, I guess, even if they are considered safer than C or C++.
  by jochenm
• I haven't seen the Lipton/Perlis/De Millo paper in years. I was around for that argument. Which really dates me. Those guys were pushing for mutation analysis.[1] That's a test for the test suite - you make some random change to the program and see if the test suite catches it. Fuzzing is related to that concept.

  It's taken way too long for verification to catch on. Here's where I was almost 50 years ago.[2] Part of the problem is that most of the interest came from people in love with the formalism. The notations used by most researchers were terrible, as is pointed out in the Lipton/Perlis/De Millo paper. You want a notation that matches the programming language.

  We had the basic architecture back then - use a SAT solver on the easy stuff, and something with some AI capability on the hard stuff. We had the Oppen-Nelson simplifier, the first SAT solver, for the easy stuff. We had the Boyer-Moore prover for the hard stuff. It's Good Old Fashioned AI, and very good for the late 1970s. The SAT solver knocks off over 90% of the verification conditions. Then you want verification notation that creates hard but abstract problems for the AI solver. Like writing two asserts in a row, with the hard problem being to prove the second one from the first.

  We didn't have enough compute back then. It took about 45 minutes on a VAX 11/780 for the Boyer-Moore prover to build up number theory from something similar to the Peano axioms. Now it takes about a second. I ported the Boyer-Moore prover to GNU Common LISP a few years ago, just to see it live again.[3]

  With LLMs to do the grunt work, this is a lot less labor-intensive. And it's really needed to keep LLM garbage under control. Given a concrete goal against which to optimize, LLM coding is much more effective.

  Formal specifications are still hard to write, but there are many important areas of software for which the specification is simple but an efficient implementation is hard. File systems. Databases. Networking. Some kinds of control systems. Stuff that really needs to work right.

  [1] https://en.wikipedia.org/wiki/Mutation_testing

  [2] https://www.animats.com/papers/verifier/verifiermanual.pdf

  [3] https://github.com/John-Nagle/nqthm

  by Animats
• Everyone knows that the weak link is the specification. But this is a spurious argument, since, by definition, if you guarantee the implementation the only thing that's left exposed is the spec itself. At least you're reducing the attack surface
  by Almondsetat
• Suppose I write a distributed algorithm in Rust. To verify it, I might describe the algorithm again in TLA+, model-check that specification, and prove that it satisfies the properties I care about.

  Now I have two artifacts:

  TLA+ specification --> proved

  Rust implementation --> runtime

  But the proof establishes something like:

  TLA_Spec => Safety

  What I actually need is:

  Rust_Program => Safety

  I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach.

  by _tgxm
• The title may be slightly misleading if you haven't bothered to read the article. It's responding to a famous paper from 1979 critiquing formal verification. The article ends up disagreeing with most of its strongest claims in hindsight, though a couple appear to remain worthwhile.
  by gr_norm
• "The counterpoint is that specifications are closer to informal requirements than implementations are (and thus a mistake is easier to spot)."

  I found exactly the opposite to be true when I took formal verification at university, and that was the major point that made formal specification / verification unattractive to me.

  by mpweiher
• I’ve been vibe coding a lot of Lean this year.

  What i found is that it is amazing once you determine and the invariants that are essential to the guarantees you want to keep.

  I built my own formally verified workflow engine, it was easy but mostly because i already knew the pitfalls and the foundational pillars of Cadence and Temporal.

  Also, it doesnt seem like common knowledge, but you can export libraries that compile to C from lean. With them you do get performant code that that has been verified and easily call them as C bindings from elsewhere.

  Lean itself does not have a good IO stack in general but its good enough for small projects.

  There is a caveat to exporting libs or native_decide in general. Once you export into C, ABI its now outside of the scope of the Lean kernel which means that bugs can creep in from the compiler itself.

  by ibarrajo
• The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.

  It is not a big deal, I think formal verification is a very useful tool to help one approach correctness, but let me explain myself. When a program is written it is trying to solve a problem, when it solves that problem correctly it has no bugs, and when it solves that problem incorrectly those are bugs. For complex problems it turns out to be very difficult(impossible) to solve them correctly. Why is there an assumption that the formal verification spec will be any more correct than the program itself? They are both trying to solve very complex problems.

  I was trying to get a feel for this by reading through the sel4 git changes trying to figure out how many bug fixes were for the OS and how many were for the spec. No real conclusion unfortunately. because they almost always have to fix both at the same time. a bug found in the OS means you have a bad spec and a bug found in the spec means your OS probably has a bug.

  by somat