What the model sees: the first level, solved

Last time I set the direction toward end-to-end confidential inference. This is the arrival: a working system you can watch, with its cryptographic core grounded in Ada and SPARK — and the deeper layers it now frees us to build.

By Pavlo Chabanov — founder of Snaga and the engineer behind its agent runtime.

---

In the last piece I set a direction: inference should be end-to-end confidential, and we should build toward it. I called the essay "toward" on purpose, because a direction is a promise, and a promise is worth exactly as much as the system that eventually keeps it.

This is that system. It's called Aspida, and the first level is solved: confidentiality now travels the whole path, it runs today, and you can watch it work. The rest of this post is about what "solved" means, where the guarantees come from, and the deeper work we're now free to do.

The first level: privacy that travels all the way through

The goal was always to extend privacy across the whole path — from your keyboard to the model and back — so that confidentiality is a property of the system rather than a courtesy of whoever happens to be hosting it. Aspida does exactly that.

Your prompt is sealed inside your browser, before a single byte leaves your device. It travels sealed across the network, it is relayed sealed through our own infrastructure, and it is opened only inside one boundary — the inference engine itself — which you authenticate against a key you pin in advance. The reply comes back the same way, sealed token by token and streamed live as the model generates it.

Everything along the path works on sealed bytes. The relay that bridges your browser to the server is a clean forwarding pipe for ciphertext. The network carries ciphertext. The hosting infrastructure stores ciphertext. Conversation history, when you choose to keep it, is sealed at rest under its own separate key, so the disk holds only sealed bytes too.

The session establishes itself in a single round trip. Both sides contribute fresh, ephemeral keys, so traffic captured today stays confidential into the future regardless of what happens to any long-term key — forward secrecy, on by default. The server proves it is the server you meant to reach by answering a challenge only the holder of your pinned key can answer, so the channel opens only with the right peer. Every record after that carries its own authentication tag, so the system accepts only intact, genuine bytes.

This is the boring, well-understood machinery of authenticated key exchange and authenticated encryption — but applied end to end, all the way to inference. That was level one, and it's done.

To be exact about what "level one" is: it's confidentiality across the whole path — keyboard, network, relay, host, disk — with plaintext exposed only inside that one authenticated boundary you pin. In the last essay I argued that a TEE relocates trust rather than removing it, because a hardware vendor's enclave stays inside the trust base. The honest read of Aspida today is that one boundary is still a boundary. Shrinking it, and bringing real confidentiality into the computation itself — the structural direction I pointed toward last time — is precisely the deeper work still ahead, not something I'm claiming as solved.

Where the guarantees come from: Ada and SPARK

The interesting part is why I can describe the path as a guarantee rather than a hope. It comes down to the foundation we chose: the trusted core — the code that holds and moves your secrets — is written in Ada and SPARK.

Ada is a language built for systems where being correct is the requirement, not the aspiration — the kind of software that flies aircraft and runs trains and stays up for decades. SPARK is the formally verifiable heart of it: a subset where properties can be proven, not merely tested. Strong, precise typing. Memory safety as a property of the language. SPARK lets us prove the cryptographic core is free of whole classes of runtime error and that it does what its contracts say — checked by a tool, not just exercised by tests.

So here is the precise shape of it. The cryptographic core — the code that seals and opens your bytes — is written in SPARK and machine-checked. The surrounding engine, the session layer, and the scheduler that decides what runs, for whom, and under which key are Ada. The raw GPU math runs in GPU kernels that the Ada core drives and bounds. The part you have to trust with your plaintext lives in those kernels; the part whose properties we can prove is the crypto core that seals it. Extending proof outward across more of the engine is part of the deeper work.

That is the whole point. When the guarantee lives in the language and the proofs, confidentiality stops being a policy you trust someone to follow and becomes a property of the code that carries your data.

Owning the engine outright buys something beyond the guarantee, too — it makes the guarantee cheap. Aspida serves a large open-weight model on a compact GPU footprint, streaming live, and its scheduler batches many sessions through each forward pass — so ten people talking at once cost far less than ten times one person. Privacy here isn't a slower, separate mode bolted on beside a faster one. You don't trade performance for confidentiality; the sealed path is the only path.

There's an honest contrast worth drawing. TEE-based confidential inference — Apple's Private Cloud Compute is the best-known example — is serious engineering, but it asks you to trust a hardware vendor's enclave and its side-channel posture. Aspida's distinct claim is different: the trusted part is an engine we wrote ourselves, with a from-scratch cryptographic core you can read and that we can prove things about, sealed on the wire — and the wire is on screen, so you don't have to take my word for any of it.

You can watch it work

This is the part the first essay could only describe and this one can show. There is a live demo. On the left, an ordinary chat. On the right, the actual bytes crossing the network — sealed records, nonces, authentication tags. Flip the server view and you see exactly what the relay and the host work with: ciphertext, end to end. The handshake happens in front of you. The keys are generated in your browser, in plain JavaScript you can read.

And you can read it where it lives. Open the client crypto — a few hundred lines of plain JavaScript with RFC references, no WebCrypto black box — and you can follow the key exchange and the sealing line by line. The same construction runs server-side in SPARK. The sealing on the right is the very same sealing that protects the chat on the left — live, real, and yours to inspect.

I want to be careful about what the demo proves. It is transparency, not the whole guarantee: code that is readable on one load can in principle differ on another from a hostile host, which is exactly why a pinned, native client is the stronger long-term story. The demo earns trust by letting you check; it doesn't ask you to assume.

The deeper work ahead

Getting the path itself confidential is what makes the deeper layers possible. With the path sealed and standing on a core we can prove things about, the work now moves inward — toward stronger formal guarantees across more of the stack, richer assurance about exactly what runs inside that one authenticated boundary, and the same privacy extended naturally from the cloud to the device and across the runtime as a whole.

There's an honesty I owe here, too. Sealing hides content, not metadata. Even with every byte encrypted, streaming a reply token by token still reveals timing, length, and shape to the host — and closing those side channels is part of the deeper work, not something the first level settles.

In the first essay I said we were heading toward end-to-end confidential inference. The path is there now — level one is solved, live, and built on Ada and SPARK — and it's the floor the harder layers get to stand on.

Try it: aspida.snaga.ai. Don't take my word for it — point your own tools at the wire and check.

— Pavlo