On software carpentry

tl;dr: “Beware of bugs in the above code; I have only proved it correct, not tried it.” –Donald Knuth

We call ourselves software “engineers”, but any sincere “engineer” who wrote more than 10,000 lines of code will tell you engineering has very little to do with what we do. We’re mostly duct-taping things.

Before building a bridge, a bridge engineer¹ computes stress, strain and deflection in their beams². A software “engineer” just starts writing code. A bridge engineer operates with a safety margin: the bridge should resist 2x to 4x the maximum expected load. A software “engineer” continues writing more code. Some of this code may be tested, for some of its input values, on some of its execution branches. But that’s about it. A bridge engineer signs off on their design³ and is subject to professional negligence lawsuits if they seriously mess up⁴$^,$⁵. A software “engineer” just ships the code.

What is the net result of our “engineering” practice? Years later, when our code leaks your phone number, home address and the names of all your family members, our “engineering” company is “deeply sorry.” This happens several times per year now⁶. If your cryptocurrency is stolen due to a hack, this is only because “we are seeing an increasing wave of sophisticated ‘cyber attacks’“⁷. We are sorry. Don’t ask us about our historical disregard for security. Shipping is more important. “Done is better than perfect”, says our PM, TPM, EM and even the CEO.

A more honest name for our practice should be software carpentry. It recognizes that, while we do have a skilled craft, safety calculations hardly enter into it. My thesis is simple and, I gather, hardly controversial by now: to graduate from “software carpentry” to “software engineering”, it would be sufficient for us to embrace formal verification⁸. Not because it’s bulletproof. Not because it will patch all holes in our software. But because it will force us to think carefully about the properties of the software we put out.

Luckily, in the LLM age, formal verification is becoming easier to apply at larger scales⁹. Our first step should be to apply formal verification to our less complex software, software with clean interfaces that admits small specifications. This would allow us to make reasonable assumptions about our software building blocks. “This library (only) sorts.”¹⁰ “This binary (only) zips.”¹¹ “This is a EUF-CMA signature scheme with no timing side-channels.” Kind of how a bridge engineer can reasonably assume that he’s been pouring concrete and not mud, you know?

Then, as our collective formal verification expertise expands, we can move on to more complex systems. “This query optimizer produces a plan semantically equivalent to the unoptimized query.” “This consensus protocol satisfies safety and liveness under \(f < n/3\) Byzantine faults.”¹²$^,$¹³ “This C compiler preserves program semantics from source to assembly”.¹⁴$^,$¹⁵

Indeed, there is plenty of formal verification work that predates the LLM age. In 2009, work on seL4 started: an OS microkernel proven functionally correct¹⁶. Sure, a few years later, we found out seL4’s specification did not account for timing channels¹⁷. Nonetheless, this is great progress: so timing channels are the only thing we have to worry about now? Fantastic! In 2015, AWS wrote a short paper explaining how they used TLA+ to model some of their system designs (e.g., DynamoDB and S3)¹⁸. Their paper insightfully points out how “in order to find subtle bugs in a system design, it is necessary to have a precise description of that design.” Absolutely! In 2017, we saw progress towards a formally verified TLS implementation that covered the full protocol state machine.¹⁹. I could keep going with more examples²⁰.

Embracing formal verification would bring many advantages. First, we could safely unleash AI to generate and optimize our code. Given that “engineers” are barely reviewing their AI-generated code anyway, why not actually enable them to safely (not) do so? It will take a bit more work. For example, we would need compiled (say) Lean programs to execute fast. But, if that doesn’t work out, we could give the “final form of software development”²¹ a try.

Second, insted of testing our code, which never covers all executions with all values²², we could prove all executions perform what we expect them to. Furthermore, instead of doing repeated, error-prone (LLM/manual) audits on our ever-changing, humongous codebases, we could reduce our audit surface to just the specs. Assuming a sound theorem proving framework²³, auditors would mostly try to poke holes through bad assumptions or incomplete modelling in the specs.

Third, and something that gets me very excited, we could obviate software dependency attacks! Instead of trusting that an imported dependency does only what we expect it to do, we would only need to update our proof after integrating the dependency. If our proof passes, then the program only does what the spec says. The “only” part seems tricky, but doable?²⁴

Lastly, I am not arguing that formal verification will be a panacea. There are many challenges. To start, some software can be as complex to specify as it is to implement (e.g., EC2 cloud architectures come to mind). Plus, all software evolves, not just in its implementation, but also in its specification. Moreover, formal verification rarely covers the full system. So, naturally, bugs will creep in the uncovered parts. For example, the compiler may still be unverified. Or, even if your software is bulletproof, the execution environment may not offer formal guarantees and let you down: e.g., your operating system may kill your process, your file system may lose your writes, your CPU may not execute instructions correctly²⁵$^,$²⁶$^,$²⁷. Even worse, the formal verification language may itself have soundness or completness issues²⁸.

But, assuming you too are a carpenter who’s tired of your chairs always breaking, what other options do you have?

Postscript

After writing this post, I keep running into evidence that the future is bleak.

On vibe spec’ing

As fate would have it, one day after drafting this post, Boris Cherny, the creator of Claude Code, tweeted that he “used Opus 5.5 to formally verify the Claude Agent SDK using Lean”.

He “sometimes combine[s] Lean and TLA+” but admits he “do[es]n’t know either language well, but [that] Claude is excellent at both.” He clearly does not understand the specs that Claude generated. (Forget about auditing them.) Is what he did useless?

From a carpentry perspective, not at all. He’ll probably find some bugs – business as usual. Good for him. Good for Anthropic.

The price paid though: confusing formal verification for abysmal verification²⁹.

How insane would it sound if a nuclear reactor engineer adopted this philosophy?

You might object: our software infrastructure should not be equated to our energy infrastructure. But this ignores how pervasive and critical (sloppy) software has become: remember CrowdStrike in July 2024?

Doubling down on software carpentry

It’s disheartening to see David Heinemeier Hansson, the creator of Ruby on Rails, doubling down on software carpentry.

Reality has a way of fighting back though.

Acknowledgements

Thanks to Vineeth Kashyap, Victor Gao, Ittai Abraham and Kobi Gurkan for their feedback on a draft version of this post.

References

For cited works, see below 👇👇