Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- The case against it is very simple: fixing your shit in software world is super easy - just release a patch! From a perspective of hardware world where fixing a single bug can cost you up to couple of million - we have for every code producing engineer up to 3 verification engineers that pseudo-randomly fuzz your design against all possible stimuli and collect coverage. Software world wouldnt bother because fixing shit is just so easy. If you regress to shipping golden CDs and next bugfix only via expansion packs - maybe you can get your shit together and start shipping good software againby artemonster
- and if producing a single CD copy would cost you a fortune then C-Suite business MBA morons would beg (or even mandate) you to use formal verification methodsby artemonster
- I was fully prepared to hate this article, given the long list of previous “I have no clue how formal proof tools work, yet have strong opinions about how useless they are” articles.
Instead, I was pleasantly surprised by how balanced it was.
What convinced me that formally proving software correct is possible were seL4, CompCert, and my own experience proving small projects correct using Lean and Rocq.
seL4: The US military and NSA tried to break seL4. They failed.
CompCert: Researchers tested CompCert against five leading commercial and open-source C compilers. Every compiler except CompCert had bugs. Not just a few, but hundreds. CompCert had zero.
And there are now many more commercial examples of software being formally proven correct.
Maybe in the future the difference between being a programmer and being a Software Engineer will be that the software you write is proven correct.
That might actually happen with the help of AI.
- I think that this is a bit of a clickbaity title but the social aspects of verification are real.
It's like 80% of the work after raising a PR is just socializing ideas and getting people to agree on stuff
by vkaku - The problem is that the people getting good results with AI-assisted formal methods are the same people who get good results with formal methods without AI assistance. They then extrapolate the benefits they are getting from AI today to what it may do for others in the future, and this is where we get into trouble.
There's a lot of art to using formal methods around how to specify the system at the right level of abstraction (to make verification tractable) and how to specify the correctness properties so they can be easily evaluated. Even with AI assistance as it currently exists, users need to know formal methods well enough to at least understand the specification of the system and the correctness properties, which requires ~90% of the effort of learning formal methods in the world before AI.
But the real hope is that one day AI will be able to use formal methods correctly on its own, benefitting those who don't know formal methods. AI can sometimes do that today, but sometimes isn't good enough for people who don't know formal methods. It is certainly possible that soon enough AI will be able to do this more reliably, but then we get into the hard problem of speculating the "AI future". It is very hard to predict what an AI that can take over the art of using formal methods cannot do. Predicting that AI will be able to do that yet not be able to collect requirements and build software autonomously, or even come up with the idea for what software to build in the first place, or even replace the software's users seems arbitrary to me. In other words, if people think AI will take care of the verification letting us focus on requirement validation, my question would be, why wouldn't an AI that knows how to verify also know how to validate the requirements? For that matter, why wouldn't it also know how to replace the users altogether?
by pron - 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
by Animats - > We didn't have enough compute back then.
The problem here is that more compute also helps testing. So it's not clear verification will pull ahead over just doing more testing, especially if there's any manual part of the verification workflow. The bugs that remain after testing become more and more difficult to stimulate.
> 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.
Mutation testing is kind of orthogonal to random input testing or fuzzing. In fact, one can use the latter to automatically kill mutants in the former, which is very useful in automatically constructing enhanced test suites. You still need to determine what the correct behavior is for each new test input.
by pfdietz - 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 surfaceby Almondsetat
- And you can put the specification in the manual of the software so the user knows what they're dealing with.by amelius
- 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 - In my opinion, it's not very different than writing an implementation of quicksort by looking at pseudocode in an algorithms book. You still need to write unit/property tests for your implementation if you want to verify it to be correct.
Any time you code up an externally specified algorithm, the onus is still on you to verify your implementation, even if the correctness of the algorithm is already verified.
by japgolly - I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place:
https://pit-claudel.fr/clement/
As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.
by black_knight - LLMs are pretty good at this. Not perfect by any means as the model is just a model after all - always wrong, sometimes useful - but the act of writing a TLA+ model helps the frontier LLMs to write correct executable code. It also works the other way around - given code, it can build a model in TLA+ and find latent bugs which it'll likely miss otherwise. (https://github.com/specula-org/Specula)by baq
- I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean
The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that
The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date
by nylonstrung - I think the reality is that it has to be baked into the language. Here's my real attempt at that - if you model the system in the language, the compiler can reason about the distributed fleet: https://hale-lang.org/proof/by rrook
- > 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.
I would say Ada SPARK solves this problem.
by JCattheATM - This is why I'm more interested in the kinds of formal methods that integrate with the actual program source code.
A couple of examples, in a rough order of approachability by a working programmer:
https://github.com/model-checking/kani
https://github.com/flux-rs/flux
https://github.com/viperproject/prusti-dev
I really wish one of these projects overcomes its academic origins and becomes a software development tool. Kani is closest to that pragmatism, but correspondingly its theory side is not quite as powerful -- though it's been getting new features that make real code easier to deal with, earlier when I played with it it could only reason about very simple functions. Flux also looked surprisingly approachable, but I haven't used it in anger yet.
There's hope that Rust will include language-level conventions for expressing contracts that all these tools can then take advantage of, because e.g. a `verus! {}` macro wrapping everything was never gonna be a viable way forward, and hopefully this will also gives us a syntax that looks like programming not math (I'm looking at you, Creusot): https://github.com/rust-lang/rust/issues/128044
by yencabulator - I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.by david-gpu
- 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 - Part of it may be that you need experience writing formal specifications just as you need experience writing programs; everyone has a lot of the second, but little of the first. They're related skills, but not the same. The first is a much more abstract (but also much more concise and powerful) method of reasoning. This sort of skill hasn't been taught well in CS education yet, owing to the fact that the underlying languages and tools were too niche.by gr_norm
- I think it very much depends on the domain. For instance, I've seen specs for floating point ops that were 1-3 pages compared to 30,000 lines of RTL. That holds pretty well for many other cases. For example, a properties like decompress(compress(x)) = x are beautifully simple compared to the details of the algorithms, and are pretty compelling correctness evidence.
- 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 - Please write an article about this.
- Did you have previous experience with formal verification and/or dependent types?by solomonb
- I'd love to know more about your experience on this, generally. What have you been doing in Lean? How have you approached this?by sroerick
- I'd love to hear more about your workflow engine, I think the expressiveness of lean and the type system makes it extremely well suited for stuff like that
I do agree that the lack of IO and libs in lean isn't really a drawback when there's a very clear interop path already
by nylonstrung - 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 - Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs.
(It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)
by inigyou