Some problems are straightforward to specify. A file system is a good example. The details of blocks and allocation and optimization of I/O are hidden from the API. The formal spec for a file system can be written in terms of huge arrays of bytes. The file system is an implementation to store arrays on external devices. We can say concisely what "correct operation" means for a file system.
This gets harder as the external interface exposes more functionality. Now you have to somehow write down what all that does. If the interface is too big, a formal spec will not help.
Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier. You start with subscript checking and arithmetic overflow, and go up from there.
That said, most of the approaches people are doing seem too hard for the wrong reasons. The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.
If you do this right, you can get over 90% of proofs with a SAT solver, and the theorems you have to write for the hard cases are often reusable.
> is that only for some problems is the specification simpler than the code.
Indeed. I had to fall back to using a proof assistant to verify the code used to build container algorithms (e.g. balanced binary trees) because the problem space gets really difficult in SAT when needing to verify, for instance, memory safety for any arbitrary container operation. Specifying the problem and proving the supporting lemmas takes far more time than proving the code correct with respect to this specification.
> If you do this right, you can get over 90% of proofs with a SAT solver
So far, in my experience, 99% of code that I've written can be verified via the CBMC / CProver model checker, which uses a SAT solver under the covers. So, I agree.
I only need to reach for CiC when dealing with things that I can't reasonably verify by squinting my eyes with the model checker. For instance, proving containers correct with respect to the same kinds of function contracts I use in model checking gets dicey, since these involve arbitrary and complex recursion. But, verifying that code that uses these containers is actually quite easy to do via shadow methods. For instance, with containers, we only really care whether we can verify the contracts for how they are used, and whether client code properly manages ownership semantics. For instance, placing an item into the container or taking an item out of a container. Referencing items in the container. Not holding onto dangling references once a lock on a container is released, etc. In these cases, simpler models for these containers that can be trivially model checked can be substituted in.
> Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier.
Agreed. The abstract machine model I built up for C is what I call a "glass machine". Anything that might be UB or that could involve unsafe memory access causes a crash. Hence, quantified over any acceptable initial state and input parameters that match the function contract, these negative specifications must only step over all instructions without hitting a crash condition. If a developer can single step, and learns how to perform basic case analysis or basic induction, the developer can easily walk proofs of these negative specifications.
It sounds really interesting.
I’ve got to disagree with this - if only specifying a file system were easy!
From the horse’s mouth, the authors of the first “properly” verified FS (that I’m aware of), FSCQ, note that:
> we wrote specifications for a subset of the POSIX system calls using CHL, implemented those calls inside of Coq, and proved that the implementation of each call meets its specification. We devoted substantial effort to building reusable proof automation for CHL. However, writing specifications and proofs still took a significant amount of time, compared to the time spent writing the implementation
(Reference: https://dspace.mit.edu/bitstream/handle/1721.1/122622/cacm%2...)
And that’s for a file system that only implements a subset of posix system calls!
I did that once, as part of a very old secure operating system project, KSOS.[1] The specs were in SPECIAL, a forgotten language from SRI International.[2] The file system had two key invariants. The weak invariant was true at the end of every write. The strong invariant was true when the file system was clean and unmounted. The job of file recovery was to take a file system for which the weak invariant was true and make the strong invariant true.
We had a spec, but nobody could prove anything about it at the time. The tools didn't exist in the early 1980s. And trying to cram KSOS into a PDP-11 didn't really fit. It ran, but was too slow. All of this was just too early. Today you can do it.
[1] https://seclab.cs.ucdavis.edu/projects/history/papers/ford78...
[2] https://www.sciencedirect.com/science/article/abs/pii/016412...
I think the core difficulty is that there's no way to know whether your spec is complete. The only automatic feedback you can hope to get is that, if you add too many constraints, the prover can find a contradiction between them. But that's all (that I'm aware of, at least).
Let's take an extremely simple example: Proving that a sort algorithm works correctly. You think, "Aha! The spec should require that every element of the resulting list is >= the previous element!", and you're right -- but you are not yet done, because a "sorting algorithm" that merely returns an empty list also satisfies this spec.
Suppose you realise this, and think: "Aha! The output list must also be the same size as the input list!" And again, you're right, but you're still not done, because a "sorting algorithm" that simply returns inputSize copies of the number 42 also satisfies this new spec.
Suppose you notice this too, and think: "Aha! Every element in the input should also appear the same number of times in the output!" You're right -- and now, finally, your spec is actually complete. But you have no way to know that, so you will likely continue to wonder if there is some additional constraint out there that you haven't thought of yet... And this is all for one of the tidiest, most well-specified problems you could hope to encounter.
Not that it's flawless either, but supplementing with standard e.g. unit tests helps catch specification bugs like this and you could generate unit test examples from the specification to review for correctness as well. You would notice problems when running the program too just like with regular programming, you wouldn't just write proofs about your program and not try running it.
Nothing is perfect but just like in regular programming languages where adding a few simple regular automated tests or some more accurate static type annotations (e.g. JavaScript to TypeScript) will catch a lot of problems compared to nothing at all (and with diminishing returns), a proof of some simple properties will flush out a lot of bugs and edge cases. So I feel the common reaction of "specifications can have flaws" is overplayed when it's clearly a big step up the process of eliminating bugs.
Does an alternative exist that's foolproof?
Great point! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.
Great point!
> supplementing with standard e.g. unit tests helps catch specification bugs like this
I don't think it does -- any specific input+output pair that a unit test tests for will satisfy all the constraints of a complete spec, so it will necessarily also satisfy an incomplete spec (i.e., a subset of those constraints). You could detect overly strong spec constraints this way, but not insufficiently strong ones.
So either that requires “generate valid code and let’s test it” or that you can write a proof statement like:
If : there is at least one implementation which is valid for the following properties, and does not meet this single property (fixed input output pair) - specifications are under defined.
Ah, I see what you mean. Yes, in practice you would have an actual implementation, and if it failed the test but passed the spec you would know the spec was underspecified. I stand corrected.
> If : there is at least one implementation which is valid for the following properties, and does not meet this single property (fixed input output pair) - specifications are under defined.
Clever! But I guess we're probably some way from being able to existentially quantify over all possible implementations... It might be that the only satisfying implementation is one for which we cannot even prove termination. More optimistically, maybe it turns out that whenever there is a satisfying implementation, there must be one in some simple class (like straight-line programs) that can be checked exhaustively.
Having a specification does not mean that one should not touch it. It is just a different level of experimental thinking.
The salient question: is risk reduced for the time alotted to write a spec in say spin or tla+?
Formal specs are risk reduction not magic.
If you don't think clearly elucidating the specific issue holding back wider adoption of an otherwise amazing technology is relevant to this discussion, I don't know what to tell you.
Regardless of the proof size, isn't the win that the implementation is proven to be sound, at least at the protocol level, if not the implementation level depending on the automatic theorem prover?
You might be able to get (a) better by requiring the LLM to feed its output through a solver and forcing it to redo anything that fails (this is where my knowledge of current LLMs kinda falls down), but (b) is still a fundamentally hard problem.
That is precisely my point.
Absolutely. See DeepSeek Prove, for instance. As far as I understand, it's basically a neurosymbolic system, which uses an LLM to write down proofs/code, then Lean to verify them, looping until it finds a proof/implementation that matches the specification, or it gives up.
Create them? Much harder.
I think most problems that one would encounter professionally would be difficult to formally specify. Also, how do you formally specify a GUI?
>The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.
I think we have to ask what exactly are we trying to formally verify. There are many kinds of errors that can be caught by a formal verification system (including some that are in the formal spec only, which have no impact on the results). It may actually be a benefit to have proofs separate from code, if they can be reconciled mechanically and definitively. Then you have essentially two specs, and can cross-reference them until you get them both to agree.
What actually happened was that some programming languages borrowed a few concepts and life carried on as before.
> There exists a higher level problem of holistic system behavior verification
This is the key observation. Strict, code-level verification of every line, while valuable in the small, doesn't contribute very meaningfully to understanding or building confidence in higher level system properties.
I see a future of modules with well defined interfaces and associated contracts. Module level contracts can be formally verified or confidently believed via property based testing. Higher level system behavior can then be proven or tested by assuming the module contracts are upheld.
Module boundaries allow for varying the desired level of confidence module by module (testing, property based testing with variable run time allotments, formal verification).
LLMs can handle each step of that chain today, allowing humans to invest specifically where we want more confidence.
No body wants to pay that price when they are struggling with product market fit.
Test tables and scenarios may not cover all the things that can go wrong (a la Goëdel), but not doing them almost guarantees broken software.
Nada Amin's Harvard webpage states;
I combine programming languages (PL) and artificial intelligence (AI), including large language models (LLMs), to create intelligent systems that are correct by construction. My current application domains include program and proof synthesis, and precision medicine. ... we look at combining Machine Learning and Programming Languages to enable the creation of neuro-symbolic systems that can move back and forth between learnable (neural) and interpretable (symbolic) representations of a system.
She was a recipient of the Amazon Research Award 2024 for LLM-Augmented Semi-Automated Proofs for Interactive Verification - https://www.amazon.science/research-awards/program-updates/7...
What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language. As a result what we get now is an informal specifications and a bunch of different final implementations for different languages. Whatever knowledge could be kept is not kept in any organized way.
A formal notation for this is a programming language. Which is why everyone use pseudo code or something equivalent for a first pass thinking or for communication.
Formal specification by itself has been tried and failed as far back as Z notation. This is a perennial problem that cannot be solved with a panacea single specification standard because it is a process problem requiring a suite of tools to verify the products plus human habits, intention, and human effort to achieve, maintain, and improve upon excellence. While standards, simplicity, and uniformity help, there is still much too much irreducible complexity and minutiae that cannot be wished away by some sort glorified Cucumber testing or inventing the N+1 thing on top of (Isabelle, Idris, Coq, etc.) that wasn't invented here.
An uncomfortable truth is that 99.99% of current software development is nowhere close to rigorous. This isn't remotely a good thing™, especially for essential components.
See also: seL4.
I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.
Formal methods are the hardest thing in programming, second only to naming things and off by one errors.