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 are proven, as theorems in the Lean proof assistant, to behave as a formal specification says: functional correctness, re-run in CI as the code changes, not merely tested. The proofs cover the wire format and delivery layers and protocol zones including the ratchets and the handshake's key derivation; those zones refine an executable model under stated assumptions about the primitives. 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 implements the published Signal protocol designs in Rust itself: the PQXDH handshake and the Double Ratchet, plus a sparse post-quantum ratchet. It does not depend on libsignal in the product. The ratchet and handshake zones are proven in Lean to refine an executable model of that specification, under stated assumptions about the primitives; 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 that implements the same protocol designs and adds machine-checked proofs that the implementation matches its specification. Tacenta does not depend on libsignal in the product. It uses libsignal only as a reference implementation to test its own against. libsignal is far more battle-tested and has seen real audits; Tacenta is younger and not yet independently audited, but gives you those proofs of functional correctness and a relay you do not have to build.
See: Assurance
Has Tacenta been audited?
No independent external 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. Until an audit reports, this is the most important limit to know.
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 properties are machine-checked against a specification you can point an assessor at. 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