Assurance you can check
Most messaging infrastructure asks you to trust a security claim. Tacenta draws the line precisely: what is machine-checked, what is tested, and what is trusted. Each claim below is stated at the strength of its evidence and no stronger, and the tier it sits in tells you what that evidence is.
Proven
Machine-checked in Lean, with no gaps in the proofs, and rebuilt by CI on every commit. Most of these are theorems about the shipped Rust itself: it is translated to Lean by Charon and Aeneas and proven to match the specification. Where a proof covers the specification but not yet the Rust, the entry below says so, because the difference is exactly the kind of thing this page exists to keep visible.
- 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.
- 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.
Tested
Verified by running the code against adversarial inputs, not by proof. Strong evidence, honestly a different kind: a test covers the cases it draws, where a proof covers all of them.
- The cryptography is used correctly
- The encryption itself is libsignal's. Using it correctly is Tacenta's responsibility, so it is property-tested: encrypt and decrypt round-trip at every size and in both directions, tampered ciphertext is rejected rather than silently mis-decrypted, and a wrong recipient cannot read a message.
- The code matches the specification
- The trust and account logic that is proven of the model is also differential-tested against the shipped Rust: randomized traces run the real code and a reference drawn from the specification in lockstep, and assert they agree at every step.
- Authentication does not leak who exists
- A sign-in with a wrong password and a sign-in for an account that does not exist take the same order of time and return the same error, so timing does not reveal which accounts are real. This is code-level reasoning backed by an empirical timing check, not a constant-time proof.
Assumed
The trusted base. Tacenta writes no cryptography of its own and makes no claim about the security of the primitives. Naming what is trusted is part of the honesty.
- libsignal, in full
- All confidentiality, integrity, and authentication come from the pinned libsignal dependency: the Signal protocol, X3DH with a post-quantum Kyber prekey, and the Double Ratchet. It is trusted wholesale, and is itself the subject of ongoing formal verification upstream. Tacenta's proofs cover the message routing and delivery around it, and say nothing about the cryptography inside it.
- The proof tools and the compiler
- The theorems assume the Lean kernel is sound, that Charon and Aeneas model Rust faithfully, and that the Rust compiler is correct. These are the standard, load-bearing assumptions of any verification effort, and they are written down rather than left implicit.
Why the line matters
A security claim you cannot inspect is a claim you have to take on trust. The value here is not that every part is proven. It is that the boundary between proven, tested, and trusted is drawn in one place and never blurred, so you can decide for yourself whether it meets your bar. For a team that has to answer for the privacy of its users, that boundary is the product.