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.
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...
This article comes close to making a fallacious argument about formal methods, which is that formal methods aren't useful unless you can exactly specify how something works.
I use model checking (a form of formal methods) daily. I separate the process into three domains: things that must be fully specified, things that can be fully specified, and things that, with the appropriate mitigation, need only have certain properties verified. Most software fits just fine in the latter category. Spend your time on fully verifying process isolation, cryptography, certain core runtime functions / behaviors, and logic relating to authentication and authorization. Everything else can be partially verified, which is much easier. Verify termination, no UB, memory safety, and that function contracts, data structure invariants, and API boundaries are followed.
A PDF implementation, a web browser, or a random server application fits cleanly into this decomposition. It matters little if the PDF is rendered oddly, or if the web browser can't interpret a page. But, it matters greatly if these errors could result in a vulnerability that could be exploited, or to a lesser extent, if these errors resulted in the software crashing.
Pure formal methods is academic. Apply engineering to this, and you get a real world and practical framework for making software safer.
Do you find that given a formal spec an agent can write complete implementation you don’t have to even read?
I keep thinking about various ways of “pushing back” on an agent, shortening feedback loop and extending what we can grantee about results.
At the most low level we can nullify probability of the next token if that token is not desirable (eg json schema enforcement under constrained inference), this is the fastest pushback. Various compiler checks, linters, unit tests, exotic type systems, e2e tests, production traces. Wondering what else is out there.
On a tangent, iirc pascal allowed single-pass compilation, so I wonder if we can embed compiler directly into inference, sort of constrained inference on steroids.
I think that reading and reviewing software is responsible.
Source code exists for humans to read first, and for computers to read second. Programming languages are unambiguous, and most languages take well to abstraction. Software can be written at a level that is appropriate for human review. Boilerplate can be avoided. It's well written when it is easy for stake holders to understand directly, without translation and without an LLM to summarize it.
Software should be the output artifact of the process, because it exactly describes the behavior of the system. The formal specification explains how the software embodiment must work, and in constructive proofs, it's even possible to extract the software embodiment from this specification. But, from a practical perspective, this is too time consuming. Instead, specification should be written to explain the rules that software must follow, instead of the exact behavior. In this case, the source code is still an important artifact, and it should be reviewed and improved upon as part of the process.
7 comments
[ 0.22 ms ] story [ 22.7 ms ] threadHowever, 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.
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...
I use model checking (a form of formal methods) daily. I separate the process into three domains: things that must be fully specified, things that can be fully specified, and things that, with the appropriate mitigation, need only have certain properties verified. Most software fits just fine in the latter category. Spend your time on fully verifying process isolation, cryptography, certain core runtime functions / behaviors, and logic relating to authentication and authorization. Everything else can be partially verified, which is much easier. Verify termination, no UB, memory safety, and that function contracts, data structure invariants, and API boundaries are followed.
A PDF implementation, a web browser, or a random server application fits cleanly into this decomposition. It matters little if the PDF is rendered oddly, or if the web browser can't interpret a page. But, it matters greatly if these errors could result in a vulnerability that could be exploited, or to a lesser extent, if these errors resulted in the software crashing.
Pure formal methods is academic. Apply engineering to this, and you get a real world and practical framework for making software safer.
I keep thinking about various ways of “pushing back” on an agent, shortening feedback loop and extending what we can grantee about results.
At the most low level we can nullify probability of the next token if that token is not desirable (eg json schema enforcement under constrained inference), this is the fastest pushback. Various compiler checks, linters, unit tests, exotic type systems, e2e tests, production traces. Wondering what else is out there.
On a tangent, iirc pascal allowed single-pass compilation, so I wonder if we can embed compiler directly into inference, sort of constrained inference on steroids.
Source code exists for humans to read first, and for computers to read second. Programming languages are unambiguous, and most languages take well to abstraction. Software can be written at a level that is appropriate for human review. Boilerplate can be avoided. It's well written when it is easy for stake holders to understand directly, without translation and without an LLM to summarize it.
Software should be the output artifact of the process, because it exactly describes the behavior of the system. The formal specification explains how the software embodiment must work, and in constructive proofs, it's even possible to extract the software embodiment from this specification. But, from a practical perspective, this is too time consuming. Instead, specification should be written to explain the rules that software must follow, instead of the exact behavior. In this case, the source code is still an important artifact, and it should be reviewed and improved upon as part of the process.