hckrnws

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.

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.

I have been formally verifying software written in C for a while now.

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

Have you made any of this work public?

It sounds really interesting.

I'm starting to. One of the libraries I've started on recently is open source. I'm still really early in that process, but I started extracting a few functions for the optimized single and double linked list containers and will be moving onto the red-black and AVL tree containers soon. Once these are done, I should be able to model check the thread, fiber, and socket I/O components.

> Some problems are straightforward to specify. A file system is a good example.

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!

Ah, they're trying to specify file system recovery, which exposes the internals.

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

> Now you have to somehow write down what all that does.

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.

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.

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?

> 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

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

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.

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.

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.

> there exist spec meeting implementations that don’t pass the test.

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.

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.

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.

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.

> And ... so what?

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.

I'm currently writing a formal model for a packet protocol in tla. (I started with spin). And im writing a paper with my findings including some thoughts on why FM are not more widely adopted. here academics and FM system devs have work to do. But let me tend to the other side: industrial developers: FM requires attention to detail in order to leverage the power of LTL etc. You mention a few things about sorting which are important details. Too many devs I think are a bit lazy here. HW does better as a discipline ... software devs no so much. FM more than vanilla coding requires attention to many small issues eg fairness. I think that too easily scares off some devs. Also writing a tla model requires a different mind set from imperative coding. Devs see that and are too allergic to learning.

Indeed, it's a microcosm of the same problem.

> is that only for some problems is the specification simpler than the code.

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?)

LLMs, at least as they exist today, could be trained to be very good at producing text that looks 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.

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

That is precisely my point.

Use them?

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

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.

I predict in 10 years „code“ that is not actually in the language of a proof assistant will be the exception, not the norm. This will happen by proof assistant languages becoming easier to the point that normal code will look cumbersome

Back when I first studied this 20 years ago the progenitors predicted it would get very popular one day.

What actually happened was that some programming languages borrowed a few concepts and life carried on as before.

I started with this 30 years ago, so yeah, I know the history :-) This time is different.

Great article!

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

Formal specification only works once the system are in a relatively final shape.

No body wants to pay that price when they are struggling with product market fit.

No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".

formal > typed > untyped > unsound > vibed

Some realized that building the tests was the more important part of writing the software long ago...

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.

And designing your code for easy testing also almost always guarantees that the code will be maintainable.

Nada Amin's research mentioned in another thread is relevant here - https://news.ycombinator.com/item?id=46252034

Nada Amin isn't relevant to hacker news, she is 15 years ahead of grifting tech bros.

Just to make sure that people don't get the wrong idea;

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

Programming is very similar to inductive reasoning, you establish some facts, do a step that changes something, and establish facts after the step and then repeat that with different steps until you get the facts you are after. (See e.g. Manber's book.) If you merely set out to rigorously write the computation steps, the result will already be a proof sufficient for a human. I am not sure, but I think Dijkstra ended up doing or maybe just writing about something like that, he wanted to get programs that were correct by construction, not proven to be correct afterwards.

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.

I wasn't familiar with that book. For other users, I think the book they are referring to is Introduction to Algorithms A Creative Approach by Udi Manber.

> What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language

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 verification methodologies are more important than some cure-all, one-ring-to-own-them-all specification.

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.

Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.

I see no need to dunk like that. There are ample stories over the years on HN how software orgs without using FM have bugs, waste money, treat people poorly, all leading to canceling software projects before delivering anything to customers. And I'm only mentioning just a very few issues. Software development in corps has many challenges to ROI and customer satisfaction.

I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.

SeL4, a number of mathematical theorems, a bunch of cryptography. You've likely trusted your life to compcert. It's not nothing, but it's admittedly a bit limited.

Formal methods are the hardest thing in programming, second only to naming things and off by one errors.

Leslie Lamport built latex, most of distributed systems such as AWS services depend on formal verification. The job of Science here is to help Engineering with managing complexity and scale. The researchers are doing their jobs

What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.

I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.

AWS talk about it a fair amount, although rarely in a lot of detail.