藍圖而非提示詞：TLA+ 如何指引 AI 編寫的程式碼

Code used to be where a team's understanding of a system lived. Now that LLMs write most of it, that understanding is quietly eroding. Here's why we're exploring formal methods at Mulga, specifically TLA+, to build better systems with AI without losing our grip on what we're building, with a real AWS EBS spec as an example.

The real contribution isn't code

It is my sincere belief that shared understanding and curated mental models are the primary artifact produced by a great engineering team.

For many, the act of sitting down to write the code was the critical step where their understanding of the problem space would SLOWLY be formalized, picked apart, and rearranged. The codebase simply provided a consistent and objective way to distribute the fruits of individual reasoning efforts to the wider team. The design discussions, frantic bug hunts, and PR reviews were core activities that served to deepen a team's understanding of how their particular problem could, and should, be solved.

At the end of it all, yes, the codebase "did the thing" (ideally). Hooray. The more important outcome was that there was now a formalized solution to the original problem, and likely many adjacent issues. Such a repository of distilled technical intent enabled later generations of engineers within the same company/group/project/community to leverage the hard-won mental models of their forebears, and ultimately drive forward the collective understanding.

Where it all went wrong

Since AI-written code became "good enough" to feasibly reach production in early 2026, many of us have been aware of the slow decline of this feedback loop that sustains our industries, livelihoods, and passions. For most of us, days now consist of prompting an LLM to produce code that satisfies a particular business need. Usually via written English. I can't speak for the entire development community, but I can personally attest to this having degraded my ability to write code by hand.

One could play devil's advocate and say something along the lines of: if LLMs can write all the code now, then why does it matter if we lose the ability to do so ourselves? To which I would say: it shouldn't really matter, provided we are able to maintain the cycle of capturing individual understanding in a manner that may be easily consumed by peers.

At last, we arrive at the core of the problem. By degrading/losing the ability to write code, we become disconnected from the act of translating ideas and intent into verifiable formalized logic that is useful to others.

The problem with natural language

How many of us regularly chat to our LLMs using the most horrendous, broken English we can possibly conceive out of sheer laziness? I'm definitely guilty! Even if you are one of the few who maintain a high quality of communication in your prompts, written/spoken language is a famously imprecise method of communication (cough synonyms cough cough).

I challenge you to try to write a system specification in your language of choice that makes explicit all assumptions and ignored details, yet leaves no room for alternate interpretations of the details that are captured. It is unlikely that you will succeed to a degree that allows you to hand that specification to an LLM and get a result that satisfies your intent.

If your system is simple enough that you do achieve an initially satisfactory result, you will inevitably discover some edge case that needs addressing. At that point, you could either adjust the written specification and have AI regenerate the implementation from scratch, which would likely resolve the issue, but also leave you with an entirely different system (unless your written spec is absurdly long and detailed).

Or you could simply ask the LLM to patch the change into the existing implementation via a quick prompt. A prompt whose core ideas are never properly understood, refined, and formalized into the collective human understanding of the project. Even if you do take the time to update the specification, fixing the edge case in isolation from the rest of the system introduces drift that severely degrades (even destroys) the spec's trustworthiness.

To illustrate the hilarity of the current prevailing approach to software specification, imagine an architect giving a construction team nothing more than a written description of the building! If natural language were precise enough to facilitate proper specifications, we wouldn't need lawyers to disambiguate the legal system for us average folk.

Formal methods and TLA+

So what do we do? How do we plug the AI-shaped hole in the bottom of the bucket that used to hold the collective knowledge of our field? Honestly, I don't know. However, my desire for a solution to this conundrum has led me deep into the formal methods rabbit hole over the past year. On my journey, I've picked up a few techniques/tools that have begun to help me address my concerns with LLM-assisted development.

One such tool that has been especially beneficial is TLA+. It was originally created by Leslie Lamport, and proves once again just how far ahead of his time he was. I'm not going to dive into an explanation of TLA+ here as it's already been done far better than I ever could, by the man himself. I highly recommend taking a moment to read Lamport's high-level view of TLA+ over on his website before proceeding. For those of you who will not heed my advice (shame), TLA+ is a language based on formal mathematical notation that allows one to create precise models of anything that can be represented as a state machine (everything, with a bit of creativity). It ships alongside TLC, which can be used to exhaustively explore logical paths within your models, and find design issues.

TLA+ is NOT code; it is mathematics. Before you recoil in disgust, here's an excerpt from Lamport's website that explains why this is so:

TLA+ teaches you that math is inherently more expressive than programming languages because it can describe a value without having to describe how the value is computed.  For example, it can describe the greatest common divisor (GCD) of two numbers as the largest positive integer that divides both numbers. This makes it possible to write a model for a specific purpose, abstracting away irrelevant details such as how to calculate the GCD. (Putting code in a procedure doesn't abstract it away; it just makes you go elsewhere to read the code, requiring that you understand the semantics of procedure call as well as the code.)

In the context of a world in which AI writes the code, this is enormously important. It gives us a language in which we can elegantly capture our intent, without getting bogged down in implementation details that ultimately don't matter to the use case. A well-written TLA+ spec is a human-readable artifact that forces the author to reason through the system they are designing in a constrained and logical format, is easy for peers to digest and iterate upon, and is objectively machine checkable (via TLC) so that LLMs are given a concrete benchmark that implementations may be evaluated against.

The TLA+ model is the architectural blueprint that the design team argues over, iterates upon, and hands to the next generation as learning material, just as the codebase used to be. The code itself becomes a concern of the construction team (coding agents). The details of the implementation can be tied to the spec, preventing drift, with the use of strategies such as trace-checking and refinement mapping. I liken these processes to the surveyor who measures a new build against the numbers in the plans to ensure conformance.

Many readers might be thinking something along the lines of "if TLA+ is so great, why haven't I heard of it before?". TLA+, and the discipline of formal methods as a whole, has largely flown under the radar of the wider software engineering community, with the exception of niche teams within resource-rich industry titans such as Google and AWS. As far as I can tell, this is mostly due to the barrier to entry.

Engineers are trained to write code. Most gave their discrete mathematics classes only the bare minimum attention needed to pass their exams, then promptly forgot the skills once they entered the workforce. From the perspective of an engineering executive: why would I have my team spend time writing a model in TLA+ (or another specification language), when I could have them build the real solution in [insert programming language of choice]? Someone would have to write the code eventually anyway...

At the time, such arguments were perfectly reasonable. No matter how precise your formal spec, someone still has to write the executable code. Or rather, someTHING! Enter LLMs. On February 5th of this year (2026), Anthropic released Opus 4.6. It is widely considered the turning point for AI-assisted development; models could finally write code that was at least somewhat reasonable. We live in a world where, if we can produce testable specifications that sufficiently constrain the details of a system that matter to the use case, we can give AI an "abstract" model and receive a working implementation with very little human babysitting.

This is MUCH easier said than done, but TLA+ is an incredible step in the right direction. And given that so many engineers are no longer writing code themselves, one could argue that improving the quality and accuracy of our specifications is a core part of the job, in a way that it never was before. I have a hunch that this mentality shift will go a long way towards breaking down the perceived "barrier to entry" that has so limited the usefulness of formal methods to the wider software engineering community.

A TLA+ specification of the AWS Elastic Block Store API

My attention at Mulga is largely focused on the storage components of our stack, Predastore (S3-compatible object storage) and Viperblock (EBS-like virtual disks). In such projects, details are extraordinarily important, and ambiguity is to be avoided at all costs. When a user engages with something claiming to be a storage service, they assume that their data is in good hands and won't be carelessly lost. On top of this responsibility, the systems are complex and easy to lose track of under the tidal wave of AI-generated contributions.

I recently used TLA+ to write a specification of the observable behavior of a subset of AWS's EBS API. The intent was to solidify my understanding of the EBS volume lifecycle state machine, so that I can ensure Spinifex (our AWS-compatible control plane) is properly adhering to the behaviors expected by the AWS CLI for the EBS operations it exposes.

For the curious reader, the specification is open source and is available to read in the Viperblock GitHub repository. It's only ~400 lines (as of now), across 4 files! This is rather notable, considering the relevant (English) technical documentation published by AWS for these operations extends across 13 separate web pages, and still manages to leave a vast amount of detail up to the reader to discern. The specification's brevity makes sense as, naturally, a written description of a building would take up far more space than a blueprint capturing the relevant details! Some request/response fields, possible error codes, and features have been abstracted out of this initial version, of course, but the core volume/attachment status state machines are captured very clearly. You do not need to be a career mathematician to make fantastic use of TLA+!

A common question I receive is "can't AI just write the TLA+ too?". Well, yes... technically. However, I'd argue there's not really any value in doing things that way. If an AI writes it, you're right back to relying on prompts that nobody has rigorously thought through, and that are invisible to colleagues and mentees.

TLA+ is ultimately a tool for the communication of ideas, in the same way that the legal system uses a constrained version of natural language to avoid confusion and mathematicians use formal notation. The power in a specification language built upon said mathematical notation is its innate ability to be applied effectively at any level of abstraction. If all you have is a vague idea of how the system you wish to build should appear to a user, that is enough to write a solid specification. There is plenty of room later to refine, and add detail that was missed (or deemed unimportant) on the first pass. This can extend as far down as the electrons themselves, if such detail is relevant to your problem space.

To illustrate this idea, here is the part of my EBS specification that captures the subset of the observable behavior of the CreateVolume operation that I was particularly interested in:

\* A client requested a new volume.
CreateVolume(req, res) ==
  /\ req \in CreateVolumeRequests
  /\ LET PossibleErrors(db) == Errors({})
         PossibleRecords    == [status             : {"creating"},
                                \* After enabling encryption by default, CreateVolume may still
                                \* see a stale value from another replica for a short window.
                                encrypted          : {db.encryptedByDefault : db \in VisibleDBs},
                                multiAttachEnabled : {FALSE}]
        \* The request was accepted.
     IN \/ /\ PossibleErrors(CurrentDB) = {}
           /\ \E vId \in VolumeIds \ usedIds, record \in PossibleRecords :
                /\ Commit([CurrentDB EXCEPT !.volumes = InsertKey(@, vId, record)])
                /\ res = [vId |-> vId] @@ record
        \* The request was rejected, possibly by a stale replica.
        \/ /\ \E db \in VisibleDBs : res \in PossibleErrors(db)
           /\ UNCHANGED vars

Some information to aid in reading this excerpt: /\ and \/ can be read as AND and OR respectively; curly braces represent a set; == is a definition; = is a comparison; the lines that begin with \E are checking whether an element exists in a target set that satisfies the condition after the :. The comments give enough of the gist that the rest of the syntax can be glossed over. Specifics can be found at learntla.com. It helps to think of a TLA+ spec as one big condition in an if statement that you would find in a traditional programming language.

This operator (an action in TLA+ terms) contains very little detail about how exactly a volume is created. In fact, throughout my entire spec, the concept of a "volume" being a virtual disk that bytes can be read from and written to is not captured anywhere! This is because it was not relevant to the control plane operations that I was concerned with at the time. I simply abstracted it away.

A final anecdote: while writing the EBS control plane model, I found myself unable to glean all of the information required to get a good picture of the possible volume status transitions from the AWS docs. This drove me to run some tests myself, and led to the discovery that a volume whose status is "creating" can immediately transition to "deleting" without first passing through "error" in certain cases. This is undocumented behavior that is extremely valuable to me in the design of Viperblock.

What's next?

At the time of writing, the spec only captures a few particularly important EBS API endpoints. I'm currently working on using TLC to trace-check my model against the real EBS API to verify that it is correct. The plan is to then trace-check Spinifex's EBS API implementation against the verified model, and fix the divergences that will inevitably be surfaced! From there I will extend the model to capture all EBS API operations that Spinifex supports, and repeat the trace-checking process.

This was not the article I initially set out to write. I'd intended to cover far more technical detail and dive deeper into the structure of the spec itself, the trace-checking methodology, and my ideas around how formal specification may be feasibly brought into the industry as a standard practice. However, in explaining my experiences to friends and colleagues, I realized that such content would not be very useful to the engineering community if I didn't first attempt to give the "why" behind the methods. Alas, the rest will have to wait for future articles.

If I have sufficiently piqued your interest, rest assured that you will not be waiting long for the next installment in this saga. So stay tuned. Until next time!

Bryn