Assurance you can check

Proven

Each claim in this section is machine-checked in Lean. The ledger lists 230 theorems, and 80 of them carry no pinned axiom list, so a change to the axioms they rely on would not, by itself, fail the build. CI rebuilds the model, proofs, committed Rust-to-Lean translation and evidence checks on every push. The translation is attested in public CI; regenerating it from Rust is a separate verification step. Where a proof covers the specification but not yet the Rust, or where a part of the system is tested rather than proved, the entry below says so.

The wire format round-trips

Every message the encoder produces, the decoder reads back intact. Wrong version, unknown type, length mismatch, and trailing bytes are rejected by construction, so a malformed frame cannot be mistaken for a valid one.

Delivery is exactly-once and in order

The delivery state machine never replays, reorders, or loses a message, and an acknowledgement can only move forward. A message counts as delivered to a user precisely when every one of their devices has read past it, and once delivered it stays delivered. The shipped Rust inherits this: it is proven to refine the specification.

The ratchet and the handshake match their specification

Tacenta's own protocol implementation is translated to Lean by Charon and Aeneas. Named operations of the Double Ratchet, sparse post-quantum ratchet, ML-KEM Braid and composed Triple Ratchet have machine-checked functional-agreement theorems against executable models, under their stated hypotheses. The classical Double Ratchet and composed Triple Ratchet receive theorems cover successful Rust results only: they do not prove that every model acceptance is accepted by Rust, or relate Rust errors to model refusals and unchanged state. Other named theorems have different scopes; the source ledger states each direction and covered branch. The same work establishes panic-freedom for named ratchet entry points under stated boundary, room and counter preconditions. The refinement proofs stop at the ratchet boundary. Separately, Session::encrypt, Session::decrypt and the two establishment entry points have panic-freedom theorems, each conditional on a contract record of 15 to 44 named hypotheses and on explicit headroom. Decrypt and the responder entry point also assume a model of the zeroize wrapper that holds derived keys. The ledger in the source gives the size of each record; the hypotheses themselves are the fields of Lean structures in the source. Thirteen primitive contracts have satisfiability witnesses, and no theorem shows that any of the four records can be satisfied as a whole. The core has also not yet linked satisfiability witnesses to every numeric size and counter precondition: by its own rough count there are some 140 bound hypotheses on some 95 theorems, in about 54 shapes. Session and prekey orchestration are otherwise modelled and tested, but not proved end to end.

Bounded session lifecycle observations hold in the model

Three Lean theorems cover a bounded abstract lifecycle: a refusal and restore leave a later honest observation unchanged; a terminal failure stays failed; and a replay has no second acceptance. The model assumes its abstract cryptographic verdicts and a committed snapshot. These are narrow L2 evidence, not a new security property or an end-to-end refinement of session orchestration.

Identity trust holds on first contact

Whatever key a device first registers is the key it stays bound to. A different key cannot displace an existing binding, and only the holder of the currently bound key can rotate it. The trust decision is proven of the shipped Rust; the recovery path around it is proven of the specification.