Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- If normal warranty rules applied to software, then software companies would be out of business very quickly.
Maybe with formal verification the laws around that can change?
by amelius - I guess in a cynical way it very well might, as it fits the bureaucratic and political mold perfectly.
Businesses would be able to rubber stamp a "Verification of Correctness", and the government could parade this political achievement around to people not knowing better, satiating their hunger for better quality software (supposedly).
In the meantime, programs would indeed feel like they became better. Except that'd be less due to them being formally verified, and more because generating all the formal verification artifacts would practically require using agents, and those agents would incidentally produce better work than what's currently typical. Not the least because people would more readily pose tough requirements to them, without regard for the difficulty.
Eventually we'd then get back where we started, with programs being flawed, just flawed in a consistent way from some arbitrary perspective (so as to still pass formal verification, of course). Since regulation would be obsessed with the rubber stamp rather than anything else, the businesses would continue to float about as usual. The only thing that'd change would be the nature of the issues.
by perching_aix - Software is buggy when people are more willing to buy the cheaper buggy software vs the higher price of more robust software.
When people want more robust software, they pay for it and it is delivered. None of the modern world would work without immense amounts of highly robust software you don't even think about, from your bank, to the airplane you fly on.
by david-gpu - > Real-world systems are too messy to be specified
I agree with this counterargument.
I mean, you can verify that Euclid's algorithm computes the GCD. Or that quicksort produces a sorted version of the input array.
But how do you verify Facebook? Facebook computes what?
For some programs, the shortest descriptions of what they do are the programs themselves.
Edit: I agree with the replies that you can verify individual parts and properties, like with testing.
by bananaflag - Yes. No Silver Bullet (1986) said that 40 years ago.by lysace
- > For some programs, the shortest descriptions of what they do are the programs themselves.
There is almost no real-world program for which this is true. One corollary of this would be that it is impossible to refactor the program to be any cleaner, which is not true for basically any large real-world program.
Another corollary of this is that no observable aspect of a program could be changed without breaking user expectations, but this too is almost always wrong (e.g. almost always, but not 100% via e.g. the famous xkcd comic about spacebar heating, a global performance optimization would be viewed as good).
by dwohnitmok - > But how do you verify Facebook? Facebook computes what?
You start by verifying the permissions structure for Facebook posts.
And by verifying the shortest, least complex functions in Facebook's server side code base.
by ocschwar - Anything with a GUI seems really daunting to specify. And then later you need to update specs to match GUI if you make any changes and you need to decide which is wrong: the implementation of the specification.by IsTom
- Well. Facebook has invested a fortune in proving that its systems follow expected properties of respecting consent—that all the data flows that happen are permitted. That turns out to be helpful for them in avoiding fines.by brians
- Facebook runs a number of quite complex internal distributed systems - databases, caches, proxies, etc. all of these are amenable to various forms of formal verification, and verifying them is the kind of thing that helps prevent outages and data loss.by dgacmu
- Agree in part, but remember that formal verification need not be done in full. By analogy, we don't avoid testing simply because everything under the sun can't be tested. Even simple things like verifying that certain API endpoints are idempotent, or as a few steps up, that the datastores used by Facebook have distributed consistency and fault-tolerance properties, are of enormous utility.by gr_norm
- With agent asssistance, we don't need writing annoying formal spec and proof anymore. Then formal verification can be a practical and useful tool in daily programming, especially for "deep module" whose spec is much simpler than implementation.by txhwind
- 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 - 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
- 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 - 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 sp1982 - 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
- 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 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