Questions and answers
Straight answers to what a developer actually asks before trusting an encryption SDK, including the parts that are not ready. Each one links to the page that shows the working.
What is Tacenta?
Tacenta is end-to-end encrypted messaging infrastructure: an SDK and a hosted relay for adding private messaging to an app. The encryption happens on your users' devices, and the relay only ever moves ciphertext, never plaintext. Its core has machine-checked Lean proofs over named security-critical zones, alongside testing for the parts not yet proved end to end. It is pre-1.0 and one-to-one only today.
See: Assurance
Who is Tacenta for?
Tacenta is for teams that have to be able to prove their privacy, not just assert it. It serves apps carrying messages where a leak is unacceptable, and where 'trust us, it is encrypted' is not a good enough answer for the people who depend on it. The verifiability is the point: it turns a security claim into something a careful engineer, or an auditor, can check for themselves. Because it is pre-1.0 and one-to-one only, it fits a focused high-assurance messaging need rather than a general chat platform.
See: Assurance
What does verifiable, or machine-checked, encryption mean?
It means named parts of the implementation have machine-checked Lean theorems stating how they agree with an executable Lean model of the written specification, re-run in CI as the code changes rather than merely tested. The proofs cover the wire decoders and named protocol operations including the ratchets and the handshake's key derivation, under stated assumptions about the primitives. Their scope varies: the classical and composed Triple Ratchet receive theorems cover successful Rust results only, while some decoder and sparse-ratchet theorems also match refusals. The core has not yet linked satisfiability witnesses to every numeric size and counter precondition, and records that whether the ratchet proofs keep their top assurance level is undecided. Session orchestration and prekey operations are modelled and tested, but not yet proved end to end. This is not a proof that the cryptography is unbreakable: the security of the primitives and the protocol design is assumed. The Assurance page marks exactly which is which.
See: Assurance
Can Tacenta's servers read my messages?
No. Messages are end-to-end encrypted on the sending device and decrypted only on the receiving device, so the relay never sees plaintext. It does handle delivery metadata, including who is exchanging messages with whom and the size and timing of each envelope, but never the contents. It routes ciphertext; it cannot read it.
See: Assurance
What encryption protocol does Tacenta use?
Tacenta builds on the published PQXDH, Double Ratchet and ML-KEM Braid designs, implemented in Rust without depending on libsignal in the product. Its wire format and KDF labels are Tacenta's own, so it is not wire-compatible with Signal. Named ratchet, codec and PQXDH key-derivation functions have scoped Lean functional-agreement theorems against executable models under stated assumptions about the primitives; the classical and composed Triple Ratchet receive theorems cover successful Rust results only. Session orchestration above them is tested rather than proved end to end. This is functional-correctness evidence, not a proof that the cryptography is secure. The primitives themselves (X25519, Ed25519, ML-KEM-1024, SHA-256, HMAC, AES) come from established Rust crates.
See: Assurance
Is Tacenta post-quantum?
Yes, in the handshake: Tacenta's PQXDH key agreement uses ML-KEM-1024 alongside X25519, so the security of a session's establishment does not rest on X25519 alone against a future quantum computer. A sparse post-quantum ratchet then re-establishes a post-quantum shared secret periodically through the session. The primitives' security is assumed rather than proven here.
See: Assurance
How do I add end-to-end encryption to my app?
Get an API key, then call the Tacenta SDK from your app: connect to your tenant, sign a user in, find another user, send. The same handful of calls exist in TypeScript, Swift, Kotlin, and Rust, and the hosted relay handles delivery while the encryption stays on your users' devices. The quickest way to see the round trip first is the CLI quickstart. It takes two commands to send an encrypted message from an API key, and the SDK section shows the same thing in each language.
See: Quickstart
What languages and platforms does Tacenta support?
Tacenta has SDK heads for TypeScript (browsers and Node), Swift (macOS and iOS), Kotlin (Android), and Rust, plus a command-line tool for trying it. All four build from the public repository: there is no npm, Maven, or crates.io package yet. The TypeScript head is the same Rust client compiled to WebAssembly, reaching the service over WebSockets. Prebuilt CLI binaries exist for macOS, Linux, and Windows.
See: SDK
How is Tacenta different from using libsignal directly?
libsignal is a mature, widely deployed library you wire up yourself; Tacenta is a hosted relay plus an SDK built from several of the same published protocol designs. Tacenta does not depend on libsignal in the product, and its own wire format and KDF labels mean it is not a drop-in or wire-compatible Signal implementation. A bundle-layer comparison with a pinned libsignal build is planned, but no cross-implementation run is recorded in the public evidence. libsignal is far more battle-tested and has seen real audits; Tacenta is younger and not yet independently audited, but provides machine-checked functional-correctness evidence over named zones and a relay you do not have to build.
See: Assurance
Has Tacenta been audited?
A review of the cryptography and code examined pinned commit d2dc386 and its report was received on 2026-09-12. Its report and the reviewer identity are not public, so this site does not count it as external assurance. It was a review, not an audit, and fixes from it are in the tacenta-core commit history. No independent audit has issued a report, and no proof-ledger engagement is underway.
See: Assurance
Does Tacenta use AI in development?
Yes. Natuvea engineers use automated and AI-assisted tools for implementation, specification text, tests and review preparation. The maintainer remains accountable for accepting changes. Tool output is project-controlled work, not an independent review.
See: Assurance
Does Tacenta help with compliance?
Tacenta holds no compliance certifications today: no SOC 2, no HIPAA BAA and no formal attestations. It makes no compliance claims. What it offers a regulated team is architectural and evidential: message contents are end-to-end encrypted, so the relay never holds readable data, and the security requirements are written down in a specification you can point an assessor at. Its evidence index marks 12 of 32 requirements as proved, 11 as tested only and 9 as assumed, and lists the evidence each proved requirement still lacks. That can support your own compliance work; it does not replace it, and you should not treat Tacenta as a certified control.
See: Assurance
How much does Tacenta cost?
There is no published pricing yet. You can create a tenant and get an API key today without a card, and run against hosted Tacenta while it is pre-1.0. How production use will be priced has not been decided or published, so do not build a cost model on today's terms.
See: Get an API key
Is Tacenta open source?
Yes. Tacenta's source is public on GitHub under the Apache-2.0 license, in two repositories: tacenta, with the SDK heads, the server, the relay and the CLI, and tacenta-core, the cryptographic core with its specification, model and Lean proofs. You can build every SDK head and run the server from them, and each repository carries a recipe to rerun its proofs yourself. The hosted service's deployment and some internal records stay private. Open source and verifiable are different things: the source lets you read the code, and the Assurance page says which parts of it are proven.
See: Source on GitHub
When is Tacenta not the right choice?
If you need group chat, a package you can install from a registry, mobile push wake-ups, or a completed independent audit today, Tacenta is not there yet. It is one-to-one only, every head builds from the repository, and it delivers to connected devices rather than waking them. There is no password reset. And if provable correctness is not something your app needs, a more mature SDK may serve you better.
See: SDK