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

Each claim in this section is machine-checked in Lean. 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 and proven to refine an executable model of the specification: the Double Ratchet, sparse post-quantum ratchet, ML-KEM Braid and composed Triple Ratchet. The same work establishes panic-freedom for named ratchet entry points under stated boundary, room and counter preconditions. These proofs stop at the ratchet boundary: Session::encrypt, Session::decrypt and prekey orchestration are modelled and tested, but not proved end to end. The ledger in the source states each one.
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.

Tested

Verified by running the code against adversarial inputs, not by proof. Strong evidence, a different kind: a test covers the cases it draws, where a proof covers all of them.

The implementation is compared with the model on named paths
Model-generated vectors run against the Rust implementation and an independent reader written from the specification. Generated sequences compare the two ratchets and the Triple Ratchet step by step, including their persisted bytes, import refusals and counter ceilings. The public ledger does not claim cross-implementation message interoperability as evidence: its supported libsignal boundary is prekey bundles and session establishment.
Decoders survive hostile input
Six coverage-guided fuzz targets and property-based decoder tests exercise hostile input. The public CI gate runs the Rust test suite, decoder properties and constant-time assembly checks; fuzzing, timing measurements and the interoperability harness run outside that gate.
Session and prekey operations are differential-tested
A clean-room reader now checks all nine agreed operation families over 27 traces and 41 steps, including prekey lifecycle and replay, establishment, authenticated send and receive, skipped-key recovery and named refusals. Five controls are required to fail. This reaches the declared bounded L2 target; it compares selected outcomes and stored state, not every possible session lifecycle or a full end-to-end refinement.
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.
Each release is exercised against the hosted service
On every release tag, the CLI binary that tag published is downloaded, checked against its checksum, and run through a full encrypted round trip against the live service, over TCP and again over the WebSocket carriage. Then each SDK head built from that tag runs the same conversation against the live service: two users sign up, message both ways and one resumes from saved state. TypeScript runs it over the carriage; the Swift Package on a Mac and the Kotlin bindings on the JVM run it over TCP and again over the carriage. The transcript of each run is kept at tacenta.com/dl/conformance/, one file per version, with the binary's hash and the service document the server answered with. It is a record of what ran, not a proof: the Kotlin head runs on the JVM rather than a device, and a pass says the shipped code did what the tests ask of it that day.

Assumed

The trusted base. This section grew in August 2026: Tacenta now implements the protocol itself rather than depending on libsignal, so more of the responsibility is ours than it used to be. That is a stronger claim to have to defend, not a weaker one.

The primitives, in full
Tacenta implements the protocol, including the handshake, the ratchets and the encodings, but writes none of the underlying mathematics. X25519 and Ed25519 come from the dalek crates, ML-KEM-1024 from libcrux, and SHA-256, HMAC and AES from the RustCrypto crates. Their security is assumed, not established here.
One primitive is ours, deliberately
XEdDSA, signing with the same key used for key agreement, is implemented in-house over the Dalek curve and signature crates. It is the single exception to the use of vetted primitive implementations and the part of the cryptography most deserving of outside scrutiny.
Not yet independently audited
No independent audit has issued a report. Findings from reviews of the cryptography and code are recorded and fixed in the open, in the tacenta-core changelog and commit history. A second review of the proof ledger waits for its four published readiness gates. The independent operation reader has reached its declared target; the remaining blocking work is semantic review of the invariant catalogue, a frozen candidate's hosted evidence and receipt, and independent claim-by-claim review of the final ledger. No external audit has issued a report, so nothing here rests on outside sign-off.
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. Some proof paths also trust Lean's compiled evaluation. These load-bearing assumptions, and the checks that constrain them, are written down.

Check it yourself

The source and the proofs are public, under the Apache-2.0 license. tacenta-core is the cryptographic core: its CLAIMS.md states what each proof covers and what it does not, and REPRODUCING.md rebuilds them. Its assurance inventory records the current evidence and its open targets; the obligation inventory names the blocking work before the proof-ledger review. tacenta is the product around it, with its own claims ledger and a recipe to rerun its proofs and checks from a clean checkout. Where this page and those ledgers disagree, the ledgers are right.

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.

Assessing Tacenta for a team

If you are deciding whether this boundary meets your application's requirements, write to info@natuvea.com with what you are building and the evidence your review needs. The reply says what exists today, where to find it, and what does not exist yet.

Get an API key Read the quickstart