Learning TLA and Quint: verifying state transitions with Temporal Logic of Actions
Posted on by Gentaro "hibariya" Terada
What is it
The other day I learned about TLA+, PlusCal, and Quint. TLA+ is a formal specification language that can be used to design, model, and verify software systems. As the name suggests (TLA: Temporal Logic of Actions), it is particularly well suited to describing state transitions and behaviors over time.
PlusCal is an algorithm language that is normally written inside a comment in a TLA+ module. Its syntax is more familiar to programmers who are used to imperative languages. The PlusCal translator converts it into TLA+, which can then be checked with the TLA+ tools.
Quint is another formal specification language for a similar purpose, with programming-language-friendly syntax, a strong static type system, a simulator, and testing support. It’s relatively new. It uses the same underlying logic as TLA+ and can use model checkers such as Apalache and TLC.
Apalache is a symbolic model checker. It translates a specification and a potential property violation into SMT (Satisfiability Modulo Theories) constraints and asks an SMT solver such as Z3 to find a satisfying execution. By default, this is bounded model checking: it searches all executions up to some specified depth.
TLC is an explicit-state model checker. It computes reachable concrete states and checks properties on them, keeping track of states it has already visited. Unlike Apalache, it does not use SMT.
Quint supports both checkers. For TLC, Quint transpiles the Quint specification into TLA+ before invoking TLC. Apalache is more directly integrated into the Quint toolchain.
Why is it useful
I’m just a software engineer, not a mathematician, but I found it useful for finding bugs in the design. I guess you don’t get many chances to code by hand these days, but you still need to design applications and think about their architectural characteristics. A flaw in the design costs more than one in the implementation details. How can you make sure your assumption is correct for all the possible state transitions in the app? Also, how can you share your idea with your teammates and agents? TLA can help you. It verifies what you define and claim in an efficient way.
Have you ever seen Die Hard 3? I haven’t. But here’s a famous puzzle in the movie: measure out exactly 4 gallons of water using only a 3-gallon jug and a 5-gallon jug. We can rephrase this as a proposition like: “There’s no way to measure out exactly 4 gallons of water using only a 3-gallon jug and a 5-gallon jug”. Then TLA tools like Quint can solve it like this:
diehard.qnt:
// Ported to Quint from a TLA+ solution in https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla
module diehard {
var big: int
var small: int
val typeOK = big.in(0.to(5)) and small.in(0.to(3))
action init = all {
big' = 0,
small' = 0,
}
action fillSmallJug = all {
small' = 3,
big' = big,
}
action fillBigJug = all {
small' = small,
big' = 5,
}
action emptySmallJug = all {
small' = 0,
big' = big,
}
action emptyBigJug = all {
small' = small,
big' = 0,
}
pure def min2(m: int, n: int): int =
if (m < n) m else n
action smallToBig = all {
big' = min2(small + big, 5),
small' = small - (min2(big + small, 5) - big),
}
action bigToSmall = all {
small' = min2(big + small, 3),
big' = big - (min2(big + small, 3) - small),
}
action step = any {
fillSmallJug,
fillBigJug,
emptySmallJug,
emptyBigJug,
smallToBig,
bigToSmall,
}
val notSolved = big != 4
}
Then you can verify your claim is true by running quint:
quint verify diehard.qnt \
--backend tlc \
--invariants typeOK notSolved
Now you can see the proposition is false, and you can actually measure out 4 gallons of water with the steps below.
[TLC] Compiling to TLA+ (via Apalache)...
...
State 1: <Initial predicate>
/\ small = 0
/\ big = 0
State 2: <fillBigJug line 45, col 15 to line 45, col 42 of module diehard>
/\ small = 0
/\ big = 5
State 3: <bigToSmall line 61, col 3 to line 62, col 55 of module diehard>
/\ small = 3
/\ big = 2
State 4: <emptySmallJug line 50, col 18 to line 50, col 43 of module diehard>
/\ small = 0
/\ big = 2
State 5: <bigToSmall line 61, col 3 to line 62, col 55 of module diehard>
/\ small = 2
/\ big = 0
State 6: <fillBigJug line 45, col 15 to line 45, col 42 of module diehard>
/\ small = 2
/\ big = 5
State 7: <bigToSmall line 61, col 3 to line 62, col 55 of module diehard>
/\ small = 3
/\ big = 4
84 states generated, 16 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 9.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-09-13 19:42:18)
This is a kind of toy problem and not practical, but my point is that when you want to express something and don’t want to deal with the ambiguity of natural language, you have a way to do that, and you can actually verify if the spec adds up. That might be useful in an era when you need to exchange an idea with agents as clearly as possible.
