Specifications Don't Exist: Why Formal Verification Hits a Wall
Galois researcher Mike Dodds argues that while formal verification works for naturally formalizable systems like compilers and microkernels, most real-world software—from web browsers to PDFs—lacks a precise, coherent specification. Drawing on his experience with DARPA's SafeDocs project, he shows how informal specs (docs, tests, slide decks) are ambiguous and contradictory, making formal verification impossible for most systems. As AI makes proofs cheap, the bottleneck shifts to specification, and we still don't know how to write one for a web browser.
The problem is that we don’t have a formal specification for Chrome, or a word processor, or even something simpler like the PDF document format.
- ivanbakel
A very valid take on spec writing. It sometimes feels like the research on formal verification is like the drunkard searching under the lamppost, in that the target is often a domain which is itself well-suited to a particular kind of computer science being done on it.
However, I think there is a middle ground between the "naturally verifiable" and the difficult cases. Certain domains, like banking apps, can want correctness guarantees about UI behaviour. A closed-off app can be very normative, so in theory specs like "the user did this action and confirmed it" can be made meaningful. But tying specs to UI is a tricky thing, and it's clearly volatile in a way function boundaries are not - apps go through redesigns, styles and elements move, etc. The abstraction of a UI as a state machine isn't hard to imagine, but actually hooking a spec into the program is a problem unto itself, and the common response is to simply ignore these problematic domains and do something easier like a backend spec that doesn't have to deal with the questions that aren't PL-shaped.
- mad44
There are now projects like Specula that, using LLMs, enable us to derive specifications from the implementation, and somewhat paradoxically, use those specifications to find bugs in the implementation.
https://muratbuffalo.blogspot.com/2026/08/specula-scaling-fo...
Secondly, I think the open partial specs, composable specs would help address the problems with monolithic specs that Dodd's cites.
https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...
- tel
I've been spending the last couple months working on a Markdown-like lightweight document format. (Short pitch, it's like Markdown but with natural extension points built in and far less subtlety).
A huge part of my goal is to write a "spec" of the format. I want it to be good enough that users can legitimately file bugs against my primary implementation for not following the spec: it is the source of truth about the language.
So, of course, I find it really interesting to discuss the grey space of "shrug, maybe this is correct". This whole process has been driving me to (a) make the language itself resilient and permissive so that it has _some_ answer for nearly all documents and (b) to constrain the output of the system such that it throws away as much information as possible, enabling us to make claims about semantics more confidently.
I don't know if I'm going to succeed at all my goals. This is sort of a small project and definitely far simpler than, say, a web browser. At the same time, it's very hard to narrow in on what it is, really, that I want such a spec to say.