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.

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.

"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.

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.

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.

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

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

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?

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

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.

> 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.

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?

Although I will admit that formal verification is looking better now than it ever did, and it's probably easier to generate proofs for those few simple safety-critical systems which benefit from it, I'm still bearish about it for the mainstream case.

I agree with "Even if fully automatic verification were within reach, it would be detrimental". Formal verification proofs make the same trade-off as overly fine-grained unit tests; they lock-down the current implementation and thus significantly reduce operational agility; because, if you make a modification to the code, you may have to re-generate the entire proof again. Proofs thus lock down sub-optimal abstractions and implementations. For many kinds of software, requirement changes are a daily occurrence and proofs would get in the way of making the required changes.

Even with complete, zero-cost automation of proof-generation, with no prompting or user-intervention (which would require the AI to have internalized a complete, perfect world-model), there would still be an incentive problem; when engineers see a lot of proofs and/or fine-grained unit tests, they are often reluctant to make the necessary refactoring to meet new requirements. Existing (counter-productive, flawed) abstractions become part of the lingo of the team and it becomes literally impossible to move off of them; yet they create a lasting barrier for new team members and when implementing new features.

The biggest problem though is that many modern software issues are flaws in the requirements (the spec itself), not in the implementation. The requirements are often produced by business people who often have a vague idea about what they want; requirements usually contain subtle contradictions or conflicts which have to be resolved.

Having worked on projects with clean, well architected code, requirements issues are by far the most common issue. On my last project, I kept coming back to my business/product co-founder with questions like: "You said that this checkbox should be on this page; but for a different onboarding flow, you said that it should be impossible for that specific user role to see/select this checkbox and the backend processing relies on this fact for reasons X, Y and Z..." or "You said to apply a filter to the collection and keep narrowing down the set as the user moves through the stages in the flow, but now you want to add a step which expands the set again with data from a different source; so now we can't just update the filter against a single collection; we need to make a separate table to hold the data from different sources; that will require some refactoring and it adds overhead since now we have to keep a lot of data per-user and we need to account for malicious spam-scenarios, etc... We can't just hold all the state in the URL (for bookmark) anymore... Users can't just share filters with each other anymore to restore the same app state across account boundaries."

In my last project, most of the work was trying to figure out what my co-founder wanted and it turns out that the idea he had in his head about the system was not logically consistent across all of its parts; a fact we only discovered after months of implementation. Also, he did not understand some of the technical limitations in terms of what kinds of data a free public API would give us access to; and that turned out to have been fundamentally incompatible with business objectives and the target market. His refusal to pivot to a premium market (where the user may have been able and willing to pay to cover the additional downstream API costs) marked the end of the project. The project was logically impossible from the start given the hard constraints of what platform to rely on, what our costs would be and what the target audience was. If we need formal verification, it would have to be for the requirements themselves, evaluated against the technical constraints. We don't need formal verification of the code.

Correct code is a mostly solved problem if you break down the typical software system into its sub-parts and identify the right platforms (e.g. CRUD, edge functions, data ingestion, data processing...) Correct requirements are a far bigger problem.

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 again

It reads like not much has changed, and given what the two underlying issues are, that's not surprising.

I've been considering getting into formal verification, but the learning curve and the illusions of rigor angle are keeping me away so far. It's great that an agent can now figure out a formal spec on my behalf and check the program it generates on my behalf for compliance, but that doesn't make me any better equipped to keep it all honest end to end. The hard part is gone, remains the hard part.

Anecdotally, what I've been doing with agents instead is I made more things declarative. Config, policy, etc. manifests can be linted for syntax and schema compliance, and the logic only has to be written once. The agents can then go ham emitting their silly little JSONs or whatever, the risk is a lot more bounded that way. Just gotta be mindful to not smuggle in too much logic, and not walking the configuration complexity clock too hard, and all remains well. I feel with agents this is now more scalable, but maybe I'll come to think different later.

i am shocked