The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.<p>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.<p>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.<p>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.<p>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.<p>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.
I have been formally verifying software written in C for a while now.<p>> is that only for some problems is the specification simpler than the code.<p>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.<p>> If you do this right, you can get over 90% of proofs with a SAT solver<p>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.<p>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.<p>> Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier.<p>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.
> Some problems are straightforward to specify. A file system is a good example.<p>I’ve got to disagree with this - if only specifying a file system were easy!<p>From the horse’s mouth, the authors of the first “properly” verified FS (that I’m aware of), FSCQ, note that:<p>> 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<p>(Reference: <a href="https://dspace.mit.edu/bitstream/handle/1721.1/122622/cacm%20(002).pdf" rel="nofollow">https://dspace.mit.edu/bitstream/handle/1721.1/122622/cacm%2...</a>)<p>And that’s for a file system that only implements a <i>subset</i> of posix system calls!
Ah, they're trying to specify file system recovery, which exposes the internals.<p>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.<p>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.<p>[1] <a href="https://seclab.cs.ucdavis.edu/projects/history/papers/ford78.pdf" rel="nofollow">https://seclab.cs.ucdavis.edu/projects/history/papers/ford78...</a><p>[2] <a href="https://www.sciencedirect.com/science/article/abs/pii/0164121281900443" rel="nofollow">https://www.sciencedirect.com/science/article/abs/pii/016412...</a>
> Now you have to somehow write down what all that does.<p>I think the core difficulty is that there's <i>no way to know whether your spec is complete.</i> The only automatic feedback you can hope to get is that, if you add <i>too many</i> constraints, the prover can find a contradiction between them. But that's all (that I'm aware of, at least).<p>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 <i>also</i> satisfies this spec.<p>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 <i>also</i> satisfies this new spec.<p>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 <i>complete</i>. But you have no way to <i>know that</i>, 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.
Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties e.g. if you only prove the list returned by a function has a certain length and nothing about the contents of the list, you're going to quickly find out when another function needs to prove anything trivial about the contents of that list.<p>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.<p>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.<p>Does an alternative exist that's foolproof?
> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties<p>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.
> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties<p>Great point!<p>> supplementing with standard e.g. unit tests helps catch specification bugs like this<p>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 <i>overly</i> strong spec constraints this way, but not insufficiently strong ones.
I think you’re picturing the unit test case the opposite way around to me, but what I see relies on having something generated for you. While a unit test case will also pass the weak specs, there exist spec meeting implementations that don’t pass the test.<p>So either that requires “generate valid code and let’s test it” or that you can write a proof statement like:<p>If : there is at least one implementation which is valid for the following properties, <i>and</i> does not meet this single property (fixed input output pair) - specifications are under defined.
> there exist spec meeting implementations that don’t pass the test.<p>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.<p>> 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.<p>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 <i>in some simple class</i> (like straight-line programs) that can be checked exhaustively.
Producing positive and negative examples is exactly where model checkers shine. I always write "falsy" invariants to produce examples of the specification reaching interesting control states for at least one input. After that, I think about the system boundaries and where it should break. Then, the model checker shows that it indeed breaks there.<p>Having a specification does not mean that one should not touch it. It is just a different level of experimental thinking.
I think you're right, but technically too many constraints doesn't mean the spec is wrong: some may be redundant, and that can be ok or even helpful. A lack of contradictions doesn't mean it's right either. I would argue that the problem of not knowing you got all the constraints specified is the same as not knowing if all generic requirements are specified. It's more work to formally specify anything and the constraints are more difficult to casually interpret, but in either case doneness is more of a continuum than a binary attribute.
And ... so what? Nobody ever said specs are error free or complete. Heck, you didn't even get into liveness, dead lock issues.<p>The salient question: is risk reduced for the time alotted to write a spec in say spin or tla+?<p>Formal specs are risk reduction not magic.
> is that only for some problems is the specification simpler than the code.<p>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?
I will just float this idea for consideration, as I cannot judge how plausible it is: Is it possible that LLMs or their successors will soon be able to make use of formal methods more effectively than humans? I don't think I am the only person surprised by how well they do at informal programming (On the other hand, there is a dearth of training material. Maybe a GAN approach would help here?)
Use them?<p>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.<p>Create them? Much harder.
LLMs, at least as they exist today, could be trained to be very good at producing text that <i>looks</i> like formal specifications, but there would be no way to guarantee that what they produced was a) correctly formed, or b) correctly specifying what was actually asked of them.<p>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.
Some already use probabilistic methods to automatically produce proofs for specifications and code they wrote manually. It’s one of the few actually useful potential use cases for LLMs.
I don't see why two LLMs together (or one, alternating between tasks) could not separately develop a spec and an implementation. The human input could be a set of abstract requirements, and both systems interact and cross-check each other to meet the abstract requirements, perhaps with some code/spec reviews by humans. I really don't see it ever working without one or more humans in the loop, if only to confirm that what is being done is actually what the human(s) intended. The humans would ideally be able to say as little as possible to get what they want. Unless/until we get powerful AGI, we will need to have technical human reviewers.
I agree, writing and maintaining specifications can be cumbersome. But I've felt that learning how to write formal specifications to keep the code in check has made me a better programmer and system architect in general, even when I do not use the formal spec tooling.
>The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.<p>I think most problems that one would encounter professionally would be difficult to formally specify. Also, how do you formally specify a GUI?<p>>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.<p>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.