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.
Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler.
Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).
It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.
The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.
From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check.
From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.
This is valid and my take is that domain modelling becomes extremely important in this context
More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket
One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with
And I think that's equally applicable to specs and business logic
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers
The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.
To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.
This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib.
It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs
There's nothing the core language lacks compared to say Haskell
I wish DX was better for people not using VS. I have my opinions about tools and when trying lean out I got the impression that you basically have to use it. They also seemingly lack a REPL.
I also got the impression that they like sticking everything into Mathlib and not splitting off smaller packages that you could use as dependencies (besides Batteries).
>why would the formal verification be any more correct than the program it is verifying?
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result
This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.
Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.
So for pedagogical purposes, can you tell us what you think the trivial spec is?
Trivial one: `forall i, j. 0 <= i < j < |sorted| -> sorted[i] <= sorted[j]`, which can be satisfied by copying a single element from `input` or by `sorted` being empty.
It can be fixed (feedback welcome) by adding: `forall i, j. 0 <= i < |sorted| -> |indexof_id(sorted, input[i])| = 1`, with `indexof_id` using equality by identity, which is crucial in practice.
Note that the amended definition implies quadratic runtime, which is the crucial difference between a specification and an efficient implementation.
but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items.
You need a way to differentiate the two 5s, that isn't present. If you had a list like:
L = [(5,foo), (2,bar), (2,baz),...]
And did a:
SORT(L, key=first) # or however it'd be specified
Then the duplicate 2s would be fine, because they're no longer duplicates, only duplicate keys. But it would still fail if (2,baz) showed up twice in the source and destination even though we've asked for SORT, not UNIQSORT.
But that's not in the specification given above. That specification is entirely wrong to specify SORT. It requires no duplicates survive the sorting process.
What is the "same one"? Define item in "I" formally.
Are we talking about Values? Then inigyou is correct.
Memory locations? Then it is trivially true, but that does not prevent me from writing 0 into every memory location.
Value + Memory location? Then it does not work for arrays since we are modifying the memory locations by moving the values between them.
The abstract notion of manipulable things in a indexable order? You need to show how that correlates to reality in a way where you can not put in a hole even larger than this one you are trying to close.
To loop back, this very discussion shows how non-trivial it really is and how much thought actually needs to be put into handling even "trivial" problems. Almost everybody who talks about how we can replace these complex implementations with simpler, understandable specifications has little to no experience with the difficulties of actually creating correct specifications. Anybody who would bring up sorting as "trivial" either has no idea what they are talking about or is so far ahead that they have weird ideas as to what constitutes as "trivial". In both cases, their opinion is highly divorced from practical reality.
That is not to say that it is not worthwhile or even that the specifications are "more complex". It is quite possible the specification is still simpler despite the difficulty, but it is also likely the complex implementation was already totally incomprehensible and a simplified specification is also incomprehensible, it is now just formally incomprehensible.
You have that /s tag, but this is actually the problem with pastel8739's spec as written.
>> 1. Every item in I is present exactly once in S
This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other.
SORT([1,1]) => [1,1]
The item 1 (which one? doesn't matter, they both do but we only need one to fail the post-condition to invalidate the result) in the source list has a count of 2 in the destination list, so this is an invalid result by the supplied spec.
pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).
However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail).
Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming.
Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.
Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.
The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.
The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations.
The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.
Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler.
E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way.
In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).
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.)
> 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 a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.
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.
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
"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.
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.
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.
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 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.
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.
Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.
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/
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
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)
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.
Something like TLA is to prove the design of an algorithm is what you intended.
Proving a specific implementation in a specific language is really the domain of that language or tools targeting that language.
In digital design for example, SystemVerilog has a whole sub-language for specifying formal properties that can be proved in simulation or with tools that prove the properties mathematically.
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.
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.
> The problem here is that more compute also helps testing.
A useful practical way to look at formal methods is "just" as testing on steroids, rather than as competition for testing. The pros and cons are mostly the same: Depending very much on their skill level, the practitioner gets a definite but finite improvement in correctness and particularly resistance to regressions, for the cost of additional upfront time and ongoing friction during maintenance. The main difference is the amount of "punch" in each passing spec requirement, which can be equivalent to an infinite number of concrete passing tests. (In the other direction: Ordinary testing using a few handpicked example (input, expected output) pairs is formal verification, just of an especially thin kind.)
Sitting in between ordinary manual tests and formal verification of entire program properties is property-based testing like Haskell Quickcheck, which offer some of the benefits of both.
Ah, but if you have specifications, you should have the ability to generate unlimited numbers of tests. Handpicked examples aren't needed. The great advance in testing with increase in compute power was the realization that carefully handcrafted tests are silly; just blast huge amounts of randomness at the system and use cheap compute to save expensive human effort.
I think it's a common experience to implement some well-defined data structure or algorithm and use the clear specification of its behavior to randomly test it, to then discover this flushes out all the bugs.
I think I cover what you're suggesting in my final paragraph?
Property-based testing is the automated spec-based random test generation you describe. It's much easier to get underway than strong formal methods that try to actually prove properties of all possible execution traces, while using many of the same powerful declarative notations, and using abundant CPU horsepower.
> the realization that carefully handcrafted tests are silly
On the downside, property-based testing won't necessarily find tricky edge cases as reliably as an experienced engineer creating individual cases manually. Specific regressions are also good to keep as "point" tests.
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?
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.
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.
Exactly, it feels dishonest that this point is so rarely brought up in essays on formal methods. You can do things like prove that all possible faults are always caught, or any memory that is accessed has first been malloc’d, or that the API endpoint will always respond (liveness). These are often both easy to specify and difficult to guarantee with conventional testing.
1) With formal verification you can prove properties about your system. With extensive testing you can also do the same but you need to take care and make sure you cover all possible cases.
2) With formal verification you can easily test things that are normally hard to cover by traditional testing. For example, if you want to test if that a postgres randomly goes offline, you don't lose any data, it's pretty hard to cover with extensive testing, whereas with formal verification you just say "postgres exists, it has state and can be online/offline, it can go online/offline at anytime" and you're covered.
To a first approximation, formal verification can guarantee some property holds for every possible run of the program, rather than just the tested ones. It's a lot more powerful than it sounds, because this unlocks the ability to talk about qualities of programs that cannot be tested (effectively or at all). Hyperproperties like confidentiality, integrity, and availability tend to be quite difficult to test, for instance.
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.
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.
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.
The final proof you get from formal methods is often irrelevant in my opinion. Most of the benefit comes from architecting the system so as much as possible can be verified and forcing yourself to make intentional decisions on the edge cases. The results are for other people.
I'm not sure you want to create a record of intentional decisions if you're at Facebook though.
> 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).
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.
I don't understand what you're trying to say here. If I sell a car that doesn't start half of the time, I can just say "well people pay more for cars that always work, you chose to spend less so you got what you deserved"?
For used vehicles, we already have that in practice; when you sell a vehicle “as is,” that’s putting a buyer on notice that that they’re going to bear the risk of future failure.
Similarly, when you buy a cooler at Wal-Mart for $25, you know it’s not going to perform the same as a $250 Yeti model.
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.
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
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 methods
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 don't think issues like syntax and schema compliance are the level of problems where verification comes into play
In this case it's more that the underlying declarative systems function as they should across any possible states or configurations
You mentioned policy and the policy language Cedar uses Lean formal verification in this way, not to verify that the specific policies users create are sound but to ensure that the declarative policy engine itself cannot produce any invalid or unwanted configurations
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.
Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler.
Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).
It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.
The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.
From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check.
From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.
This is valid and my take is that domain modelling becomes extremely important in this context
More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket
One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with
And I think that's equally applicable to specs and business logic
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
> Does Lean have a type for "list containing only prime powers"?
You can wrap a base type with a proof which is called bundling
inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n)
So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers
The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.
To some degree these are the same things, depending on the type system. But it might be easier to write a function accepting a list of size 3 than matching on a constraint, which might get separated from the variable it annotates.
Lean is a dsl for mathematicians, not computer programmers.
This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib.
It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs
There's nothing the core language lacks compared to say Haskell
I wish DX was better for people not using VS. I have my opinions about tools and when trying lean out I got the impression that you basically have to use it. They also seemingly lack a REPL.
I also got the impression that they like sticking everything into Mathlib and not splitting off smaller packages that you could use as dependencies (besides Batteries).
Yeah I really dislike that you need neovim or VS to benefit from Infoview
Haven't tried it but there's this community-made REPL https://github.com/leanprover-community/repl
>why would the formal verification be any more correct than the program it is verifying?
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result
This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.
Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.
So for pedagogical purposes, can you tell us what you think the trivial spec is?
Trivial one: `forall i, j. 0 <= i < j < |sorted| -> sorted[i] <= sorted[j]`, which can be satisfied by copying a single element from `input` or by `sorted` being empty.
It can be fixed (feedback welcome) by adding: `forall i, j. 0 <= i < |sorted| -> |indexof_id(sorted, input[i])| = 1`, with `indexof_id` using equality by identity, which is crucial in practice.
Note that the amended definition implies quadratic runtime, which is the crucial difference between a specification and an efficient implementation.
Ok, I’ll bite, why is this wrong?
For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that:
1. Every item in I is present exactly once in S
2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.
SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6
I'm sorry, do all 5's look the same to you!! /s
aka, one item in I is missing in your output.
No, if it had one more 5 it would violate your specification that every time must occur exactly once.
Also, SORT(1,2,3,4) = 1,2,3,4,7
Not my specification (drive by third party)
but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items.
> Also ...
Yeah, that needs tightening up by pastel8739
You need a way to differentiate the two 5s, that isn't present. If you had a list like:
And did a: Then the duplicate 2s would be fine, because they're no longer duplicates, only duplicate keys. But it would still fail if (2,baz) showed up twice in the source and destination even though we've asked for SORT, not UNIQSORT.In the cases of
one or both of those might be incorrect ?( I'm teasing, perhaps )
More seriously,
> You need a way to differentiate the two 5s
As there's no unique filtering or other reduction going on here, there's a permutation chain from input to output.
But that's not in the specification given above. That specification is entirely wrong to specify SORT. It requires no duplicates survive the sorting process.
The specification said
5 is an item in I, and it is present exactly once in S.and 5 is another item in I, and it's not present in S.
Yes it is, it's right there, between the 4 and the 6.
That's not the same one - track the permutation chain.
What is the "same one"? Define item in "I" formally.
Are we talking about Values? Then inigyou is correct.
Memory locations? Then it is trivially true, but that does not prevent me from writing 0 into every memory location.
Value + Memory location? Then it does not work for arrays since we are modifying the memory locations by moving the values between them.
The abstract notion of manipulable things in a indexable order? You need to show how that correlates to reality in a way where you can not put in a hole even larger than this one you are trying to close.
To loop back, this very discussion shows how non-trivial it really is and how much thought actually needs to be put into handling even "trivial" problems. Almost everybody who talks about how we can replace these complex implementations with simpler, understandable specifications has little to no experience with the difficulties of actually creating correct specifications. Anybody who would bring up sorting as "trivial" either has no idea what they are talking about or is so far ahead that they have weird ideas as to what constitutes as "trivial". In both cases, their opinion is highly divorced from practical reality.
That is not to say that it is not worthwhile or even that the specifications are "more complex". It is quite possible the specification is still simpler despite the difficulty, but it is also likely the complex implementation was already totally incomprehensible and a simplified specification is also incomprehensible, it is now just formally incomprehensible.
> I'm sorry, do all 5's look the same to you!! /s
You have that /s tag, but this is actually the problem with pastel8739's spec as written.
>> 1. Every item in I is present exactly once in S
This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other.
The item 1 (which one? doesn't matter, they both do but we only need one to fail the post-condition to invalidate the result) in the source list has a count of 2 in the destination list, so this is an invalid result by the supplied spec.pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).
1. The output is a permutation of the input.
2. If the comparison implements a strict total order, the output is sorted according to it.
You are correct.
However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail).
Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming.
Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.
See how easy it is once you have right terms ;)
Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.
The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.
do you have a reference to anywhere that discusses this further? It seems pretty trivial to me
Often the spec can be simpler than the original.
The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations.
The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.
Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler.
E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way.
In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).
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.)
> 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 a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.
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.
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
I'd love to know more about your experience on this, generally. What have you been doing in Lean? How have you approached this?
Did you have previous experience with formal verification and/or dependent types?
"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.
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.
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.
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 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.
It’s been renamed recently. Maybe a few times. I think it’s rocq now. [1]
[1] https://rocq-prover.org/docs
Huh, I missed all of that. The linked discussion about the renaming from your link was a bit odd: https://discourse.rocq-prover.org/t/coq-community-survey-202...
It seemed to me from the survey that most people didn't want it changed or didn't care, but due to anglophone users they decided to change it anyway.
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.
> 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.
Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.
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/
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
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)
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.
Something like TLA is to prove the design of an algorithm is what you intended.
Proving a specific implementation in a specific language is really the domain of that language or tools targeting that language.
In digital design for example, SystemVerilog has a whole sub-language for specifying formal properties that can be proved in simulation or with tools that prove the properties mathematically.
Apply this to building a house and complaining that the architecture drawings don't include the technical drawings.
The two are different artifacts for different jobs. The same is true for code and architecture. That they have an impedance mismatch is a feature.
It would be even better if there was a machine that could take your architecture and technical drawings and alert you of any mismatches.
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
> 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.
> The problem here is that more compute also helps testing.
A useful practical way to look at formal methods is "just" as testing on steroids, rather than as competition for testing. The pros and cons are mostly the same: Depending very much on their skill level, the practitioner gets a definite but finite improvement in correctness and particularly resistance to regressions, for the cost of additional upfront time and ongoing friction during maintenance. The main difference is the amount of "punch" in each passing spec requirement, which can be equivalent to an infinite number of concrete passing tests. (In the other direction: Ordinary testing using a few handpicked example (input, expected output) pairs is formal verification, just of an especially thin kind.)
Sitting in between ordinary manual tests and formal verification of entire program properties is property-based testing like Haskell Quickcheck, which offer some of the benefits of both.
> Ordinary testing using a few handpicked example
Ah, but if you have specifications, you should have the ability to generate unlimited numbers of tests. Handpicked examples aren't needed. The great advance in testing with increase in compute power was the realization that carefully handcrafted tests are silly; just blast huge amounts of randomness at the system and use cheap compute to save expensive human effort.
I think it's a common experience to implement some well-defined data structure or algorithm and use the clear specification of its behavior to randomly test it, to then discover this flushes out all the bugs.
I think I cover what you're suggesting in my final paragraph?
Property-based testing is the automated spec-based random test generation you describe. It's much easier to get underway than strong formal methods that try to actually prove properties of all possible execution traces, while using many of the same powerful declarative notations, and using abundant CPU horsepower.
> the realization that carefully handcrafted tests are silly
On the downside, property-based testing won't necessarily find tricky edge cases as reliably as an experienced engineer creating individual cases manually. Specific regressions are also good to keep as "point" tests.
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
And you can put the specification in the manual of the software so the user knows what they're dealing with.
But can you make a mere user read and understand that specification?
Not all users are the same and that's OK. Just like not everybody needs to read and verify the Linux kernel.
Also note that a specification can be input to other tools, such as a formal verification system for an encompassing system.
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.
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.
Exactly, it feels dishonest that this point is so rarely brought up in essays on formal methods. You can do things like prove that all possible faults are always caught, or any memory that is accessed has first been malloc’d, or that the API endpoint will always respond (liveness). These are often both easy to specify and difficult to guarantee with conventional testing.
I’m a bit confused as to what makes formal verification different from extensive testing.
1) With formal verification you can prove properties about your system. With extensive testing you can also do the same but you need to take care and make sure you cover all possible cases.
2) With formal verification you can easily test things that are normally hard to cover by traditional testing. For example, if you want to test if that a postgres randomly goes offline, you don't lose any data, it's pretty hard to cover with extensive testing, whereas with formal verification you just say "postgres exists, it has state and can be online/offline, it can go online/offline at anytime" and you're covered.
To a first approximation, formal verification can guarantee some property holds for every possible run of the program, rather than just the tested ones. It's a lot more powerful than it sounds, because this unlocks the ability to talk about qualities of programs that cannot be tested (effectively or at all). Hyperproperties like confidentiality, integrity, and availability tend to be quite difficult to test, for instance.
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.
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.
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.
There are approaches to GUI which are closer to formal specification than what is currently in use. Look at HotDrink for instance: https://tt.utu.fi/soft/hotdrink-gui-programming-with-dataflo...
I’m not even sure what would be gained by formal verification of a GUI
> 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.
The final proof you get from formal methods is often irrelevant in my opinion. Most of the benefit comes from architecting the system so as much as possible can be verified and forcing yourself to make intentional decisions on the edge cases. The results are for other people.
I'm not sure you want to create a record of intentional decisions if you're at Facebook though.
> 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).
Yes. No Silver Bullet (1986) said that 40 years ago.
I’ll add that all the glorious specs we wrote last week is can and will be useless tomorrow. No spec survive real life vanity
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?
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.
I don't understand what you're trying to say here. If I sell a car that doesn't start half of the time, I can just say "well people pay more for cars that always work, you chose to spend less so you got what you deserved"?
For used vehicles, we already have that in practice; when you sell a vehicle “as is,” that’s putting a buyer on notice that that they’re going to bear the risk of future failure.
Similarly, when you buy a cooler at Wal-Mart for $25, you know it’s not going to perform the same as a $250 Yeti model.
They're saying the software that makes the car start was more expensive than the software that allows you to play music in the car.
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.
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
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 methods
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 don't think issues like syntax and schema compliance are the level of problems where verification comes into play
In this case it's more that the underlying declarative systems function as they should across any possible states or configurations
You mentioned policy and the policy language Cedar uses Lean formal verification in this way, not to verify that the specific policies users create are sound but to ensure that the declarative policy engine itself cannot produce any invalid or unwanted configurations
i am shocked