Composition and Modular Verification of TLA+ specs
Preamble. This post came slowly, simmering over months really. So there is some stream of consciousness in here, and a lot of deliberating in public. The post is me learning modular verification and talking myself into it at the same time. Even pep-talking myself, because this is genuinely hard, and the field's standard advice is to avoid modular verification. But the advice is due for revision: LLMs plus TLAPS are quietly changing the economics that made monolithic spec the rational default.
The compositionality problem
TLA+ is compositional in the abstract sense... In the astral plane, a program execution is an infinite sequence of states, each state giving a value to every variable in an imagined universal state space. A spec is a predicate (yes/no test) on executions, which denotes a set of allowed executions. In this setup, the steps that change variables in other specs look like stuttering to yours. And that enables us to denote composition as a beautiful purely logical conjunction, Spec1 /\ Spec2.The problem is, this is too pure. When you try to model check a conjunction of two specs, your astral travel gets grounded. Since TLC only accepts specs in the normal form Init /\ [][Next]_vars, you need to manually expand the conjunction of two boxed formulas as:
[][N1]_v1 /\ [][N2]_v2 = []((N1 \/ UNCHANGED v1) /\ (N2 \/ UNCHANGED v2))
Expanding this gives us joint steps for N1/\N2, solo steps for each side, and both side stutter steps (which can be omitted vacuously). However, shared read/write variables between N1 and N2 cause problems (which we have ignored conveniently in the first paragraph, and now it is time to face them). Suppose a producer and a consumer share a channel. The naive producer spec Init /\ [][PNext]_<<chan, produced>> says: if chan changes, it was one of my actions. If you conjoin that with a consumer that also writes chan, you have specified a system where the consumer can never take a value. Conjunction of closed specs over shared state leads to over-constraining like that.
Open specs
The fix is to write each component as an "open" spec, a term I should define, since it has taken some damage lately. In an open spec, every step is either one of my actions or an environment change I have agreed to live with. E.g., in the producer component, EnvTake is the producer's "rely", i.e., the changes it tolerates from the rest of the universe. Yep, this is pretty much rely-guarantee reasoning: the Env action is the assumption/rely, and your actions plus your invariants are the guarantee.
Send == chan = NoVal /\ chan' = produced /\ produced' = produced + 1
/\ UNCHANGED acked
EnvTake == chan # NoVal /\ chan' = NoVal /\ acked' = acked + 1
/\ UNCHANGED produced
Spec == Init /\ [][Send \/ EnvTake]_<<chan, acked, produced>>
PSync == /\ (chan = NoVal) => (produced = acked)
/\ (chan # NoVal) => /\ produced = acked + 1
/\ chan = produced - 1
The consumer specification is symmetrical and straightforward.
Recv == /\ chan # NoVal /\ consumed' = Append(consumed, chan)
/\ acked' = acked + 1 /\ chan' = NoVal
EnvPut == /\ chan = NoVal /\ acked < MaxSend
/\ chan' = acked /\ UNCHANGED <<acked, consumed>>
Spec == Init /\ [][Recv \/ EnvPut]_<<chan, acked, consumed>>
CSync == acked = Len(consumed)
In the composition, you do the obvious thing. You drop each component's Env disjunct and replace it with the other component's concrete actions. The INSTANCE keyword allows us to refer to Producer/Consumer formulas in the composed state space. The entire glue module is this:
P == INSTANCE Producer
C == INSTANCE Consumer
Init == P!Init /\ C!Init
Next == \/ (P!Send /\ UNCHANGED consumed)
\/ (C!Recv /\ UNCHANGED produced)
PSpecOK == P!Spec
CSpecOK == C!Spec
Note that dropping the Envs and composing like this works only legitimate if each side's concrete actions are behaviors the other side's Env permitted. That's the obligation we state in the discharge module. The same two INSTANCE lines appear in the discharge module below to denote the obligations that each component's actions must imply the other's Env action. That is, the consumer's Recv must be a legal EnvTake from the producer's point of view, and vice versa.
vars == <<chan, acked, produced, consumed>>
DischargeTake == [][ (C!Recv /\ UNCHANGED produced) => P!EnvTake ]_vars
DischargePut == [][ (P!PSync /\ P!Send /\ UNCHANGED consumed) => C!EnvPut ]_vars
Modular verification is doable
Modular verification is within reach of standard TLC, although it is rare to see it practiced due to feasibility reasons which I will revisit at the end.
First, notice where the discharge obligations get used. In the composition, Recv => EnvTake must hold at every step the composed system takes, i.e., at every reachable state of the composed system. But computing those reachable states means building the composed state space, which is exactly what modular verification refuses to do. How do we work around this?
Below is a rely-guarantee workflow that achieves this. Note that our cross-component discharge obligations are single-step implications. This is guaranteed for safety relies, because an Env action is a predicate on state pairs. A liveness rely like "the environment eventually takes the value" would not fit in an action, and is out of scope here. So, instead of calculating the reachable states, we can check the obligations over the crudest enumerable over-approximation, "all type-correct states", and strengthen the hypothesis only when a counterexample forces us to.
Step 1. Model check each component alone, closed by its own Env. This has very small state space, as the other component's private state never appears. This establishes local invariants (PSync for the producer). And if your rely is strong enough, this establishes even some global properties. E.g., my consumer proves in-order delivery against its EnvPut.
Step 2. Check the rely discharges as action implications over a "chaos universe", a throwaway spec whose Init admits every type-correct state and whose Next admits every type-correct transition. Checking [][Recv => EnvTake]_vars against chaos verifies the implication over all state pairs, without computing reachability.
TypeUniverse == /\ chan \in Vals \cup {NoVal} /\ acked \in 0..MaxSend
/\ produced \in 0..MaxSend /\ consumed \in SeqUniverse
Init == TypeUniverse
Next == /\ chan' \in Vals \cup {NoVal} /\ acked' \in 0..MaxSend
/\ produced' \in 0..MaxSend /\ consumed' \in SeqUniverse
ChaosSpec == Init /\ [][Next]_vars
\* The two discharge obligations are checked as properties here
DischargeTake == [][ (C!Recv /\ UNCHANGED produced) => P!EnvTake ]_vars
DischargePut == [][ (P!PSync /\ P!Send /\ UNCHANGED consumed) => C!EnvPut ]_vars
Step 3. Conclude verification by induction. This one is a theoretical step, as you do not run TLC here. The argument is this: every step of the composition is one side's action, and by (2) that step is also the other side's Env step. So each step extends both open specs at once, and by induction the composition refines both, and thus every property established in (1) transfers to the composition. This may seem a bit circular: the producer's guarantee licenses the consumer's assumption, which licenses the producer's guarantee. But, the induction breaks the circle: each side's guarantee holds one step longer than the assumption it feeds, which is precisely the semantics of Abadi-Lamport's -+> operator.
Now let me come clear about the kink here, and the explanation for PSync in DischargePut obligation. My consumer's rely, "the environment delivers exactly the next expected value", was too strong. Discharging it against the producer's Send over the chaos universe failed with the TLC counterexample "produced = 5, acked = 0", which means the producer is about to send value 5 to a consumer expecting value 0.
Note that only the chaos universe contains this state. No real execution contains it, because every Send bumps produced, every take bumps acked, and a one-slot channel keeps two such counters in lockstep (equal when the slot is empty, one apart when full). And that is the embodiment of PSync property.
PSync == /\ (chan = NoVal) => (produced = acked)
/\ (chan # NoVal) => /\ produced = acked + 1
/\ chan = produced - 1
I didn't pull PSync out of a hat. It is the Producer invariant we checked locally in step 1 for the Producer open specification. Since PSync mentions only producer-visible variables, the producer-alone check from step (1) establishes it for free. The dischargeable obligation becomes PSync /\ Send => EnvPut, and TLC confirms this.
Is it worth it?
Earlier I said modular verification is rarely seen in practice, for feasibility reasons. In 1997, Lamport wrote a paper titled "Composition: A Way to Make Proofs Harder", and as always he is on the money. The mainstream TLA+ answer to decomposition follows his advice. Instead of decompositional verification, the practiced approach is to write one abstract specification of the whole system and verify that. The monolith needs no Env actions, it can cut across component layers wherever modeling is most convenient, and TLC handles the state space without problems since the specs are written at high (often too high) levels of abstraction. This is much simpler than specifying components and conjoining them, with all the bookkeeping for shared variables and joint steps we did in this post. Moreover, the costs of modular verification land on the human upfront: decomposition is hard, interface abstraction is hard, and both must be finished before you can check anything.
Despite all this, I am coming to believe we should perform compositional and modular verification anyway, because the monolith buys its simplicity by ignoring the system's actual structure, and we should not trade away good system design to appease the verifier. Interfaces, ownership boundaries, and independently evolving components are not verification inconveniences, they are the system design. A verification habit that only works on monoliths trains us to specify protocols with the system design erased. And ignoring good design causes all sort of problems for sustainability and reusability of verification.
Let me try to explain this better. In an earlier post, "The Two Abstractions of System Design: Hide or Reduce", I argued that we conflate two abstractions: modularity abstraction hides (interfaces, encapsulation, vertical boundaries), while modeling abstraction reduces (cut the system to the minimal behavioral skeleton relevant to a property).
The rely-guarantee reasoning we used in this post is where the two abstractions meet and become a joint constraint. The modularity abstraction is the boundary: we split the specs into private versus interface variables, hiding produced from the consumer and consumed from the producer. The modeling abstraction is the Env actions. E.g., EnvPut is not an API for the producer, it is a reduction of the producer: the minimal behavioral skeleton of the entire producer relevant to the consumer's property.
In that post I noted that a well-designed artifact can sometimes serve simultaneously as a spec to refine against and a skeleton to reason from. In rely-guarantee this is our exact mechanism. The same EnvPut is used twice: as a skeleton when the consumer verifies against it, and as a contract when the producer's actions must be shown to refine it.
So good interface design finds the seam where a modularity cut and a modeling slice coincide. Interface design is hard because it is the one place the two abstractions must agree. Instead of complaining that abstractions leak, the Env action specifies the behavior about which interleavings cross the boundary, and proves guarantees on top of it.
With the LLMs helping us in verification, this is becoming feasible. And with the LLMs generating the code, which needs reusable modular verification, this is becoming necessary.
One more thing... TLAPS changes the economics
Everything above was standard TLC, with the assumption that proofs are expensive and impractical. But they no longer are, again thanks to LLMs.
I tried TLAPS on these obligations, with Claude writing the proofs for the discharge obligations, and tlapm checking them. I re-check these from the VSCode command palette to prove step/module, and it was very satisfying to watch them all turn green.
The benefits of proofs scale well. Proof effort tracks the length of the spec, not the size of the state space. In our case, the chaos-universe caps go away: PSync /\ Send => EnvPut now holds for all counters, all values, and all instantiations. Modularity also works well for TLAPS. Modular decomposition produces many small local lemmas instead of one big invariant, and even the paper induction from step (3) can be mechanized to make the whole composition argument a checked artifact. Modular proofs also handle change well. When a component is modified, the broken obligations tell you exactly which contract clauses changed.
The spec files and proofs are on Github:
Hillel Wayne (hi Hillel!) wrote an accessible introduction to composing TLA+ specifications with state machines: https://www.hillelwayne.com/post/composing-tla/
Also here is an excellent talk from Ron Pressler on composition and conjunction of specs:
https://www.youtube.com/watch?v=TP3SY0EUV2A
Finally I enjoyed discussing with Markus Kuppe and Ugur Yavuz about TLAPS!
Comments