Proving safety of Tendermint consensus with Apalache and AI

This text is artisanally typed using Das Keyboard, with occasional suggestions by Copilot (most of them ignored anyways). The figures are generated with ChatGPT 5.5.

If you read my previous blog post, you know that I was impressed by the ability of the frontier AI tools to write complete proofs of safety for the Ben-Or's consensus using Lean 4 and TLAPS. Not everything went smoothly. Also, I gave the tools an inductive invariant in TLA⁺ as a starting point. This inductive invariant was almost correct, except that it needed a fix in one of the lemmas for the general case of .

As in the previous blog post, here I used Claude Code Opus 4.8 and Codex GPT 5.5. I refer to them as "C1" and "C2", without disclosing which is which. I have not tried Fable and GPT 5.6 in this experiment.

Next stop: Tendermint. Ben-Or published his paper in 1983. It does not look like this algorithm has a modern implementation, though implementations of randomized BFT consensus protocols exist. Hence, I thought of trying the same approach with a modern BFT consensus protocol that runs in the wild. Tendermint is the most obvious candidate for this experiment. It has a formal specification in TLA⁺, which I wrote with Zarko Milosevic in 2020, back at Informal Systems. This specification even has lemmas for an inductive invariant in TLA⁺.

This blog post completes my Gestalt with the Tendermint specification. Back in 2019-2020, I checked the specification for small parameter values such as , , and . Since the Cosmos blockchain (powered by Tendermint) was running hundreds of validators, Ethan Buchman (co-founder of Cosmos and CEO of Informal Systems) was asking me, whether we could transfer the results to in the range of hundreds. Back then, it meant either doing further research on threshold automata, or writing a proof of safety in TLAPS. Again, this did not fit the company's business priorities. Now, this is done in just a week of work with AI tools.

Did I just ask Claude Code or Codex to write a proof of safety for Tendermint? Well, there was an obstacle to that. In 2022, Rodrigo Otoni found that Apalache was reporting counterexamples to inductiveness for our invariant TypedIndInv, which was supposed to be inductive. Since the inductiveness check was taking hours, it was not included in the Github CI workflows, so we missed the moment, when it stopped working. It's hard to tell what happened back then. The Tendermint implementation was going through upgrades, but then repository was reverted at some point. Perhaps, the reverted specification was not the latest one. Also, we fixed several soundness issues in Apalache since 2020. Maybe, the invariant was not inductive in the first place. Moreover, the time effort for fixing the invariant was not clear, and fixing it was not the business priority anymore.

In the following sections, I give a bit more details about the process of fixing the inductive invariant and generating the proofs.

Need this kind of work for your protocol?

I help teams turn distributed-system behavior into executable specs, model-checking campaigns, and CI-ready conformance harnesses. I can also help your team to pick up TLA⁺ and related tools as well as to explain where your verification efforts may run into a bottleneck.

Discuss your system

1. Fixing the inductive invariant

In any case, to write the proofs, I had to fix the inductive invariant first. A few years ago, fixing the inductive invariant meant the following:

Run Apalache,
stare at the counterexample,
think about the consensus protocol and why the invariant was not strong enough,
fix the invariant and repeat.

Obviously, the part of the process that included "staring at the counterexample" was not automated at all.

This time, I decided to avoid the pain and feed examples from Apalache into C1, in order to strengthen the invariant. This does not require any additional tool support from Apalache. The tool can already generate example behaviors, not just counterexamples to invariants. This is an often overlooked feature of Apalache.

As a first step, I was running Apalache to generate example states that satisfy TypedInvInv. Then, I was asking C1, whether these states presented feasible states that were reachable from the initial states as defined with Init. This way, C1 added seven additional lemmas.

Once the states looked feasible, I started to produce counterexamples to inductiveness of TypedIndInv with Apalache. C1 identified the key fix to the problematic lemma by changing one of the thresholds and excluding nil values:

- \* if T + 1 processes precommit on the same value in a round,
- \* then in the future rounds there are less than 2T + 1 prevotes for another value
+ \* if 2T + 1 processes precommit on the same valid value in a round,
+ \* then in the future rounds there are less than 2T + 1 prevotes for another value.
PrecommitsLockValue ==
      \A r \in Rounds:
-         \A v \in ValidValues \union {NilValue}:
+         \A v \in ValidValues:
              \/ LET Precommits == {m \in msgsPrecommit[r]: m.id = v}
                 IN
-                    Cardinality(Senders(Precommits)) < THRESHOLD1
+                    Cardinality(Senders(Precommits)) < THRESHOLD2
              \/ \A fr \in { rr \in Rounds: rr > r }:  \* future rounds
-                    \A w \in (ValuesOrNil) \ {v}:
+                    \A w \in (ValidValues \ {v}):
                         LET Prevotes == {m \in msgsPrevote[fr]: m.id = w}
                         IN
                             Cardinality(Senders(Prevotes)) < THRESHOLD2

After the key fix, C1 added three more lemmas to strengthen the invariant, and then Apalache was not reporting any counterexamples anymore. The whole process of fixing the inductive invariant took about 2 calendar days.

Details. Actually, before fixing the inductive invariant, I decreased the scope of the specification to the original Tendermint. The existing TLA+ specification has additional features such as evidence collection and the accountability invariant. I did not want to run into the rabbit hole of reasoning about the evidence sets. Hence, the file tendermint-single-indinv.tla contains the specification of the original Tendermint without the additional features, as well as the fixed inductive invariant. The TLA⁺ specification is generated from two specifications in a Python DSL: tendermint-single.py and tendermint-single-indinv.py. This is not really relevant for this story though, as the AI tools work well with TLA⁺ as well as with the Python DSL. Moreover, once the invariant was fixed, the AI tools effortlessly transferred the fix to the original TLA⁺ specification.

2. Generating TLAPS proofs

Once the inductive invariant was fixed, I asked C1 to bootstrap the proofs of inductiveness of TypedIndInv. After that, I was switching between C1 and C2, when they were reaching the 5h limits. In contrast to the Ben-Or's consensus, the proof process for Tendermint was relatively uneventful. Perhaps, C1 and C2 know way too much about Tendermint. The only interesting assumption was that the proof required exactly . In total, it took me about 5 calendar days to have working proofs. You can find the complete proofs in tendermint-single-indinv-proofs.tla. The proofs are about 4.6 KLOC. One can argue that the inductive invariant constitutes the core of the proof. The definitions related to the inductive invariant are about 400 LOC.

As always, it was fun to read Claude's status updates on the proof progress:

I've verified this wall exhaustively enough to characterize it precisely. Let me stop grinding and give you a straight assessment rather than more thrashing.

The orientation normalization dissolved the congruence wall.

The statements of the main theorems mirror the technique of inductive invariants:

THEOREM InitInd ==
  Init => TypedIndInv

THEOREM Inductive ==
  ASSUME TypedIndInv, Step
  PROVE  TypedIndInv'

THEOREM AgreementThm ==
  TypedIndInv => Agreement

The assumptions section is where we should be really careful. It easy to constrain the problem to a much simpler one. For example, in one of my experiments, the LLMs constrained the problem to , which would make the proofs as strong as the model checking results by Apalache. Obviously, we want to prove the theorems for the general case.

These are our assumptions:

\* The actual number of faulty replicas. The spec declares no `F` constant, so we
\* define it here as the cardinality of the Faulty set.
F == Cardinality(Faulty)

\* TLAPS' standard proof of natural-number induction uses Isabelle. This workbench
\* runs without an Isabelle backend, so we trust the induction principle instead of
\* replaying that library proof. Needed for the round induction in Section D.
AXIOM NatInductionTrusted ==
  \A Q \in [Nat -> BOOLEAN] :
    (/\ Q[0]
     /\ \A n \in Nat : Q[n] => Q[n + 1])
      => \A n \in Nat : Q[n]

\*****************************************************************************
\* NAMED ASSUMPTIONS
\*
\* The Apalache spec declares no module-level ASSUME. We state the parameter
\* constraints the proofs rely on under names, so steps can USE/cite them.
\* Resilience (confirmed with the spec author): N > 3*T /\ T >= F /\ F >= 0.
\*****************************************************************************

\* Tendermint/BFT resilience: strictly more than three times the fault bound.
ASSUME NgtT == N > 3 * T

\* The optimal BFT replica count (confirmed by the spec author). REQUIRED for quorum
\* intersection: with a fixed 2T+1 quorum threshold, two quorums share a *correct*
\* process only when N = 3T+1. Without it QuorumsIntersectInCorrect is FALSE, e.g.
\* N=5, T=1, F=1, A={c1,c2,f}, B={c3,c4,f}: both have size 2T+1=3 but meet only in
\* the faulty node; agreement fails for N>3T+1 (a 2T+1 quorum is below 2/3 of N).
ASSUME Neq3Tp1 == N = 3 * T + 1

\* The actual number of faults is bounded by T.
ASSUME TgeF == T >= F

\* The number of faults is non-negative.
ASSUME FnonNeg == F >= 0

\* Correct and faulty replicas are disjoint.
ASSUME DisjointCF == Corr \cap Faulty = {}

\* Cardinality is only meaningful for finite sets; there are finitely many replicas.
ASSUME FiniteCF == IsFiniteSet(Corr) /\ IsFiniteSet(Faulty)

\* N counts all replicas (correct + faulty), which are disjoint.
ASSUME NCard == N = Cardinality(Corr) + Cardinality(Faulty)

\* The protocol parameters are natural numbers.
ASSUME ConstNat == N \in Nat /\ T \in Nat /\ MaxRound \in Nat

\* Nil is encoded as -1 and is not a valid value. (Confirmed by the spec's use of
\* -1 as the nil sentinel throughout; TODO: confirm with the spec author.)
ASSUME NilNotValid == -1 \notin ValidValues

\* There is at least one valid value to propose. Needed by the base case for the
\* existential witness inside AllNoEquivocationByCorrect over empty message logs.
ASSUME ValidValuesNonEmpty == ValidValues # {}

As you can see, is redundant in the presence of . The assumption of is consistent with the paper. The case of has a simple counterexample to agreement, and Apalache finds such a counterexample. If we want to make it work for , we have to change THRESHOLD2 from to .

Stabilizing the proofs. Surprisingly, I found that the generated proofs were going through on the virtual machines, where I run C1 and C2, but they were failing on my host machine. Surprisingly, it was taking SMT longer on my host machine to prove certain goals than on the virtual machines. I asked C1 and C2 to stabilize the proofs.

3. Conclusions

I believe we only start to see what is possible at the intersection of TLA⁺ and AI tools. Obviously, the AI tools help with usability a lot. Running TLA⁺ tools and writing TLAPS proofs is way easier now.

When it comes to Tendermint, the obvious next steps would be:

Extend the specification and the proofs with multiple heights (blocks),
Extend the specification and the proofs with timeouts and liveness properties.

If you are interested in specification and verification of consensus protocols or other protocols, contact me.

Want to talk?

If you want to pick up my brain for a few hours, drop me an email. After that, we can switch to a messenger of your choice or have a call. You can see my portfolio at konnov.phd.