Verifiable encrypted messaging

Encrypted messaging,
with a proven core.

Encrypted messaging your developers can check, not just trust. Don't take our word for it. Take the proof you can run.

Explore the SDK Run the quickstart
Machine-checked in Lean: the wire codec and delivery state machines, proven against a spec. What that covers, and what it doesn't.

Start where you are

01 · Try

Prove the hosted path

Create a test tenant, install the CLI and send an encrypted message between two users before you write any application code.

Run the quickstart

02 · Build

Choose a native SDK

Start in TypeScript, Swift, Kotlin or Rust. Each head has the same core surface, a runnable guide and generated API reference.

Browse the SDKs

03 · Assess

Inspect the evidence

Read what is proven, what is tested and what is assumed before you decide whether the boundary meets your application’s requirements.

Read the assurance record

The SDK in a few lines

A tenant handle connects to your service. A client represents one signed-in user on one device: it finds other users, sends, receives and carries its encrypted state across launches. 

const tenant = await Tacenta.connect("tct_your_api_key");
const alice = await tenant.signIn("alice", "correct horse");

const bob = await alice.find("bob");
if (bob) await alice.send(bob, "hello");

for await (const message of alice.inbound()) {
  console.log(message.from, message.text());
}

TypeScript shown. The same tenant-and-client model is available in every SDK head, with language-native asynchronous APIs.

Read the developer docs Create a test tenant

Built for apps that cannot leak

Tacenta is for teams handling messages where the server cannot read the content, and where the evidence behind that promise matters. The relay sees ciphertext and delivery metadata; encryption keys remain on the devices that send and receive.

The core implements the published Signal designs, including a post-quantum ML-KEM prekey and sparse post-quantum ratchet. Its assurance record draws the line between the parts that are machine-checked, tested and trusted.

See the assurance boundary