Molt Petit

A deliberately small BFT consensus protocol with recursive certificates, deterministic finality and light clients that never need to replay history.

The implementation is Rust, imported into Lean 4 and machine-checked. The same validator source also instantiates the recursive proof circuit.

The consensus core of Ledger.

The protocol

There are n fixed participants, and slot s belongs to participant s mod n. A chain is valid if every matured window of n slots contains at least ⌈2n/3⌉ blocks.

A light client keeps only a recursive certificate and a short recent suffix. It accepts them if the certificate verifies, the suffix is valid and sufficiently dense, and its tip is no more than n slots behind the client's clock. Blocks n deep are final.

That is essentially the entire agreement rule, not a sketch of it. The deliberate smallness is where Molt Petit gets its name.

What that gives you

• Byzantine fault tolerance. Up to ⌊(n−1)/3⌋ Byzantine slots in each n-slot window.
• Fast, deterministic finality. A block n deep is final, with no probabilistic confirmation tail. With n = 7 and ~4-second slots, this takes roughly a minute.
• No voting rounds. No quorum certificates, view change, randomness beacon or longest-chain fork choice: one round-robin schedule and one density rule.
• Offline light clients. A client can stay offline for as long as needed, then synchronize in milliseconds by downloading a constant-size artifact: one recursive certificate plus a short recent suffix.

Keys in practice

The consensus rule itself is small. Most of the paper is about what has to be true around it for that rule to remain safe in a real deployment.

The security model is deliberately explicit about operational assumptions: what an operator has to protect, when keys may rotate, what happens after a key is stolen, and what discipline is required for the Byzantine-fault-tolerance guarantee to continue to hold.

The adversary is allowed to control Byzantine participants and, in the stronger model, occasionally steal a current signing key. The goal is not to assume that this never happens, but to state precisely what an operator has to do so that compromise is contained and eventually stops mattering.

In particular, theft of a current signing key can heal after a confirmation-gated rotation.

That is why key rotation occupies so much of the paper: the protocol is deliberately tiny, while the operational contract needed to run it safely is spelled out in detail.

What is actually machine-checked

The validator is written in Rust and imported into Lean 4 through Charon + Aeneas. The light-client safety and forged-time results are connected to that runnable implementation rather than proved only about a separate hand-written model.

The validator is written once over a small backend abstraction. The same source is used both by the native implementation and to instantiate the plonky2 recursive-proof circuit, so the circuit enforces the predicate that was verified.

There is also a second implementation in TypeScript, imported through an independent pipeline and proved sound to the same model.

What it costs

The simplicity comes with deliberate restrictions:

• Fixed membership. The participant roster is closed and equally weighted. Signing keys rotate; roster seats do not.
• Synchronous slots. The light-client safety statements use a recency rule relative to the verifier's clock.
• No liveness recovery. If participation falls far enough that a matured window misses the density threshold, the chain stops instead of switching leaders or repairing itself with fork choice.
• Predictable leaders. Slot ownership is public and deterministic rather than stake-weighted or selected by a VRF.

These are deliberate trade-offs for a small, known operator set where deterministic agreement and very small client state matter more than open participation.

Molt petit is Catalan for "very small."