Engineers who care about getting a distributed protocol right write it twice — once as a formal model a checker can explore, once as real code — and nothing keeps the two in agreement, so the effort spent proving the design correct buys much less than it should; PGo (UBC) closes that gap by extending the PlusCal modelling language with a clean separation between the system being designed and the environment being assumed about it, which is precisely what lets a compiler tell which half is real code and emit runnable Go from the same source the model checker reads.
The argument in one glance
-
Problem
Distributed protocols are hard to get right, and the proof and the program are different things
Production distributed systems ship with bugs that degrade performance, take services down and lose data, because the space of possible interleavings is far too large to reason about by hand. Formal methods answer this: write a model of the protocol, state the properties it must satisfy, and have a tool explore every reachable state. Amazon and others do exactly this. But what gets checked is the model, and what runs in production is a separately hand-written program. Nothing connects them, so the design drifts the moment anyone tunes anything, and the confidence the checking bought quietly evaporates.
-
What people did
Prove the translation too, with a theorem prover
Frameworks like Verdi and IronFleet do close the gap properly. They formalise the relationship between a specification and an implementation and let you prove, in Coq or Dafny, that the code refines the design. This is a genuine success and the guarantees are the strongest available. Systems built this way really are verified end to end in a way nothing else is.
-
Why it fell short
The rigorous route costs person-years and needs a proof engineer; the shortcut hits state explosion
The paper counts the effort: a verified Raft key-value store took 3 person-months in Ivy, 12 in Verdi, and 18 in IronFleet. That is not a budget an ordinary engineering team has, and these tools are complex enough that they are essentially research instruments. The alternative the systems community reached for instead — model-check the implementation directly — is fundamentally handicapped, because an implementation has vastly more state than a model and the checker drowns. So formal methods for distributed systems stay influential and largely unused.
-
This paper's idea
Make the model compilable by separating the system from what it assumes about the world
PlusCal, the readable front end to TLA+, cannot be compiled because a model freely mixes the protocol with a description of its environment — a network modelled as a buffered queue sits in the same code as the server logic, and no compiler can tell which is which. Modular PlusCal adds three things that draw the line: archetypes, which contain only the system and cannot touch global state; resources, which are the named holes where environment dependencies plug in; and mapping macros, which fill those holes with arbitrary model-level behaviour for the checker. Now the compiler knows exactly which half to emit, so the same source produces both a checkable model and running Go.
Why this problem is worth solving
The whole value proposition of formal methods for systems rests on an assumption that usually is not true. Exhaustively exploring every reachable state of a model to see whether it satisfies stated properties, reporting a concrete counterexample trace when it does not. It is the approachable end of formal methods — you write the model and the properties, and the tool does the rest without needing guidance — but it is bounded: the state space must be made finite, so what you check is the model within limits you chose, and a theorem prover, which can reason about infinite state spaces symbolically, gives stronger guarantees at the cost of requiring far more human direction.
What makes the gap hard to close is that a model deliberately contains things that must not become code. A procedural language that compiles to TLA+, letting engineers describe a protocol with familiar constructs — loops, conditionals, processes — rather than writing raw temporal logic. Its distinctive feature is labels, which mark blocks of statements that execute atomically and become single transitions in the generated model. Labels are the designer main dial: more of them means more possible interleavings and so a more realistic model, at the cost of a state space that grows exponentially.
What people did before, and where it broke
- Model the design, then write the implementation by hand. This is the mainstream practice, including at companies that take formal methods seriously. Where it broke. The two artifacts have no mechanical relationship. Every implementation-level optimisation is an opportunity for them to diverge, and nothing detects it when they do — so the checking result decays over the life of the system.
- Prove the refinement with a theorem prover. Verdi and IronFleet formalise the model-to-code relationship and let you discharge it in Coq or Dafny. Where it broke. Cost and accessibility. The paper’s comparison puts a verified Raft key-value store at 12 and 18 person-months in these frameworks. The authors also note that introducing threading into a system verified this way can require redesigning the correctness properties and rewriting the proofs — so the verification actively resists the performance work you will inevitably want to do.
- Model-check the implementation instead of the model. If the code is what runs, check the code. There is impressive work here. Where it broke. State explosion. An implementation carries orders of magnitude more state than a model of the same protocol, which is precisely what modelling exists to strip away.
- Extract code from an existing modelling language. The natural question: why not just compile PlusCal? Where it broke. PlusCal has almost no support for abstraction or information hiding, so a single model interleaves the lock server logic with the buffered-network semantics used to check it. A compiler reading that source has no way to know which statements describe a system and which describe an assumption about the world.
- The gap. Nobody had asked what a modelling language would need in order to be compilable. The obstacle was not compiler technology but the language design — specifically, that a model has two kinds of content in it and no way to tell them apart.
How PGo turns one source into two artifacts
From a mixed model to a checkable specification and a running program
-
-
new
-
new
-
new
-
new
-
new
The idea
The obstacle was never compilation, it was that a model contains two kinds of thing. This is the observation the whole paper turns on, and once stated it is obvious. A model of a lock server contains the lock server, which is a real design that should become code, and a model of the network, which is a claim about what the world does and must never become code. PlusCal offers no way to say which is which, so the two sit interleaved in the same file. Modular PlusCal adds exactly enough structure to draw the line — archetypes that cannot see global state, resources as declared holes, mapping macros as the checker-only filling for those holes — and having drawn it, compilation becomes straightforward. The result is that a designer writes one artifact rather than two, and the properties the checker established are properties of the thing that runs. Closing the distance between what a person writes down and what a machine executes, by designing a language whose structure a compiler can act on, is the same move as the collective communication language work covered elsewhere on this site.
The generated code has to refine model semantics that are stricter than a real machine. The hard engineering is here. A PlusCal label is an atomic step, and a real execution must behave as though those steps interleaved in some total order — which means a critical section that touches several resources either commits entirely or leaves no trace. The runtime therefore treats each critical section as a small transaction: at its end it asks every resource involved to pre-commit, commits them all if they all agree, and otherwise aborts and rolls everything back. That is a genuine cost, because a section containing two network sends now needs something like atomic broadcast, which nobody deploys. So the design supplies an explicit weakening pathway — a relaxed resource can stub out the pre-commit check when the developer knows a single operation cannot half-fail. The paper is unusually candid that this enlarges the trusted computing base and moves the running system away from the specification it was derived from, and that automating the soundness of these relaxations is future work. Building the escape hatch into the design rather than pretending nobody will need it echoes the concurrency-bug work for Go covered elsewhere on this site, which is aimed squarely at the layer this one deliberately does not verify.
Checking, unlike proving, survives contact with performance work. The most persuasive argument in the paper is almost incidental. Having built the Raft key-value store, the authors wanted more throughput, so they restructured the model into several communicating processes each dedicated to one task — and then simply re-ran the checker. In a theorem-proving framework the same change can require redesigning the correctness properties and rewriting proofs, because a prover needs guidance and the guidance is itself an artifact that must be maintained. A bounded checker needs less information to begin with and therefore adapts more easily. That is a weaker guarantee bought deliberately in exchange for agility, and it is what lets a verified system be tuned rather than frozen. Choosing a cheaper analysis that keeps up with a changing artifact, rather than a stronger one that resists change, is the same trade drawn from the opposite direction by the causal-ordering work for dynamic analysis covered elsewhere on this site, which gives up static guarantees entirely in exchange for watching what actually happened.
Walking a critical section through the runtime
Executing one atomic label of a compiled model
A section that updates a shared queue and sends a network message — two operations the model says happen together or not at all.
Step 1 of 5
The main loop begins a critical section
Generated Go is not a whole program but a collection of implementations, one per label in the model, plus metadata. A hand-written library supplies the loop that drives them, handles the jumps between labels, and manages the resources each section touches.
Keeping the compiler minimal is deliberate. PGo emits largely unoptimised code and defers configuration to runtime, on the reasoning that the compiler and its library are part of what you must trust — so the less of the complexity lives in the generated output, the better. What PGo claims to eliminate is protocol bugs, not bugs in input and output code.
Why it works
- The separation is what makes compilation decidable at all. An archetype cannot reach the surrounding global state, so everything it needs from outside arrives through declared parameters → the compiler can identify exactly which code is system and which is assumption → the same source serves a checker that wants the assumptions and a compiler that must discard them.
- Resources are one abstraction serving two masters. In the model a resource is filled by a mapping macro describing what the environment might do; at runtime the same hole is filled by a real socket or store → the interface between design and world is named once and instantiated twice → no separate glue specification is needed to relate them.
- Treating a label as a transaction is what refines the model honestly. The model says a labelled block is one atomic step → implementing it as pre-commit across all involved resources, then commit or roll back, makes a real execution serialisable in the same way → the running system exhibits behaviours the checked model allows.
- A minimal compiler shrinks what you have to trust. The generated code is deliberately unoptimised and defers linking to runtime → complexity concentrates in a hand-written library that can be scrutinised once and reused → the claim is narrowed to protocol correctness, which is where the checking actually applies.
- Bounded checking adapts where proofs must be rewritten. Restructuring the model into more concurrent processes changed the design substantially → re-running the checker required no new guidance, because a checker needs less information to start with → performance tuning and verification stop being in tension.
What it costs (trade-offs and scope)
- The performance is well short of production, and the paper says so. Against etcd, a widely deployed Raft key-value store, PGo-RaftKV reaches 21% of the throughput at comparable latency. Two causes are given: etcd implements a threaded extension of Raft allowing far more concurrency than the core protocol specification PGo follows, and the immutable data structures required by TLA+ semantics carry real overhead.
- One system is not close at all. The primary-backup key-value store peaks at 340 operations per second against more than 50,000 for Redis in synchronous replication mode. The stated cause is the absence of batching, which would require a more complex set of correctness properties than the authors had time to write.
- The modular composition is both unverified and slower. Linking two separately checked models is done by hand, the combination is explicitly not verified, and the composed Raft store performs worse than the monolithic one — a little below the best related work. The authors offer that some of the gap might be tuning effort rather than composition overhead.
- The development-effort comparison is anecdotal and the authors flag it. The 1 person-month against 3, 12 and 18 figures are self-reported, produced by graduate students in their first and second years, and the paper explicitly says these numbers are anecdotal and not representative of the average developer, calling for user studies.
- The trusted computing base is large. You must trust the two compilation paths, the model checker, the hand-written runtime library, your own bootstrap Go code, the Go runtime and scheduler, and — when combining separately checked components — that the combination is sound. Relaxed resources add to this further.
- Checking is bounded and the bounds are small. The Raft configuration assumed 3 servers, one election round, at most two committed log entries and at most one node failure. That finds real bugs and is a much weaker statement than a theorem prover makes.
- Several baselines were difficult or impossible to run. Working C++ could not be extracted from the Ivy model with any version of the tool, so measurements use pre-extracted files from an author archive. Two other systems suffer buffer overflows on larger messages, so a reduced-value variant of the benchmark was used for them. Verdi primary-backup system had no runtime glue ever written. Two further candidate systems turned out to be model-checking targets rather than working implementations.
- Timing lives outside the verified region. Election timeouts and retry delays were tuned by hand in Go because the model does not reason about physical time — which is exactly where a large class of distributed systems bugs lives.
The evaluation
Four routes from a distributed protocol design to running code
| Property | Model, then implement by hand | Theorem-prover frameworks (Verdi, IronFleet, Ivy) | PGo (checked model compiled to Go) |
|---|---|---|---|
| What the guarantee covers | |||
| Effort for a Raft key-value store | Not measured — but two artifacts written and maintained separately | ||
| Throughput against related verified systems | Not applicable | ||
| Throughput against production systems | Whatever you build | Not compared directly | |
| How well it survives performance tuning | Trivially — but the model becomes stale |
Check yourself
Check your understanding
1. Why can a standard PlusCal model not simply be compiled into running code?
2. Why does the runtime treat each critical section as a small transaction?
3. What is the practical argument for using a bounded model checker rather than a theorem prover here?
4. How do the performance results compare against production systems?
Sources
The paper is “Compiling Distributed System Models with PGo” by Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do and Ivan Beschastnikh, published at ASPLOS 2023 Volume 2, pages 159-175, DOI 10.1145/3575693.3575695. All authors are at the University of British Columbia, and the paper carries an artifact appendix and a data-availability statement.
This explainer is written from the full text, read through a proxy of the ACM Digital Library copy. Everything above comes from the paper’s own sections 2 through 7: the trusted computing base discussion enumerating what a developer must trust on both the model and implementation sides, including the unverified combination of separately checked components; the background on TLA+, PlusCal and the trade-off labels present between realism and state-space growth; the argument for why PlusCal cannot be compiled directly, with the running lock server example; the three new abstractions of archetypes, mapping macros and resources, with the reliable ordered link macro shown as a pair of TLA+ operators; the code generation strategy including the deliberate minimalism of the compiler, the hash-array mapped tries used for compound values, and the critical-section pre-commit and commit protocol with its relaxation pathway; the fault-tolerance discussion via developer-supplied failure detectors; the modular composition of a Raft model with a key-value store model and the statement that the contract between them is the user responsibility; the effort table with its 1 person-month figure against 3, 12 and 18, together with the authors caveat that these are anecdotal and unrepresentative; the model-checking configuration bounding Raft to three servers, one election round, two committed entries and one failure; the YCSB evaluation on Azure against Vard, IronKV, Ivy-Raft and etcd, including the 41% throughput and 42% latency figures, the 21% of etcd throughput, the difficulties extracting working code from the Ivy model, and the buffer overflow issues that forced a reduced-value workload variant; the primary-backup comparison at 340 against more than 50,000 operations per second; and the CRDT comparison showing the SoundCloud implementation up to twice as fast.