ENC — Litepaper

Abstract

The apps you use were built for a world where humans wrote the code, humans reviewed it, humans ran the servers, and humans clicked the buttons. That world is ending. Software is increasingly written by AI and operated by autonomous agents at machine speed — and every assumption the old app stack rested on (trust the operator, someone reviewed the code, your data lives in their platform) collapses at once.

ENC — encode, encrypt, enclave — is the substrate for what comes next: a trust-minimized, self-sovereign protocol where code is verified, not trusted, data carries its own proof, and apps are generated from one proven spec.

Verification doesn't stop at the protocol. The infrastructure and apps are formally verified too, because they're all generated from the same proven mathematical core — their guarantees hold by mathematics, not by trusting whoever (or whatever) wrote the code. So one specification, reviewed once, expands — instantly, across ~10 platforms — into a running app whose security is carried by proof, not re-audited by hand.

The same machine that generates a verified messenger generates a marketplace, wallet, social feed, or registry — AppGen redefines existing apps as agent-native, trust-minimized, sovereign ones. A sovereign messenger is simply the first instance, not the product.

I. The paradigm is breaking

Every app today runs on infrastructure you have to trust. The operator can silently rewrite your data, censor you, lock you out, or vanish — and you can't check. Even "audited" or "decentralized" systems still ask you to trust that the code actually running matches what was reviewed, and that the operator behaves.

That bargain held while four things were true: code was human-written, it was human-reviewed, apps were operated by accountable people, and they were used by humans who would notice when something looked wrong. All four are now false:

• Code is AI-written — "vibe-coded" faster than anyone can read, let alone audit. No reviewer — not the best engineer, not the best mathematician — keeps pace with what machines now emit; human review, the old basis of trust, simply doesn't scale to machine output. You can't validate what no one fully read; "we reviewed it" becomes a statement about a fraction of the code, at a point in time.
• Apps are agent-operated — autonomous agents act on your behalf and transact with other agents, at machine speed, across parties that have never met. There is no human in the loop to apply judgment.
• Trust doesn't compose to machines — reputation, terms of service, and a careful read are human-scale instruments. They don't survive millions of unattended interactions. And the human method for building trustworthy systems — theorize a clean spec, then hand-write the code and hope it matches — can't keep pace with machine-scale output either; it's the wrong instrument for the job.
• Claims have to leave the room — a screenshot proves nothing to anyone who wasn't there. The instant your data must be trusted by someone else's system, "trust me" fails.

When neither the operator nor the code can be vouched for by a human — because no human can keep up — the only trust that scales is mathematical proof. Trustworthy infrastructure for agents must be built with output checked by math, not by reviewers. That is the forcing function behind everything in this paper.

II. The new paradigm: trust-minimized, self-sovereign, verifiable

ENC replaces the old bargain with three properties, each the forced answer to what the agent era broke:

• Trust-minimized (the system property) — you trust as little as possible. Not "trustless" (there's always some trusted base) — minimized to a small, explicit, measurable surface, with everything above it backed by proof.
• Self-sovereign (the outcome you own) — your identity, data, and money are yours: encrypted, portable, no phone number, no central account, no operator that can censor or revoke you.
• Verifiable (the mechanism) — every piece of data and every line of running code can be checked, not believed: authentic, ordered, unaltered, authorized — by you, a counterparty, another app, or an agent, without trusting the source.

Skip any one and the stack collapses:

III. The protocol

ENC is, at its core, small and sharp: an event-sourcing store you own — signed writes ordered into append-only logs, committed to structures anyone can verify, governed by explicit permissions.

Declarative, not computational

An ENC node runs no app code. State is non-computing — key→value leaves in a Sparse Merkle Tree — governed by a single manifest that declares everything an app is: its states, traits, operations, readers, and lifecycle. The node doesn't execute an app; it enforces a declaration — verify, check, append, update. This keeps the system verifiable (no arbitrary computation to reason about) and fast (bounded, predictable work per event).

Virtual enclaves

The unit of an ENC app is an enclave — a self-sovereign realm for your data. The name echoes a hardware TEE (like SGX), but inverted: an ENC enclave is protected by cryptography and math, not silicon. It's a cryptographically-defined, append-only log that is yours — writes authorized by your keys, data portable. Reference templates express every app shape: Personal (profile / identity anchor), DM (private mailbox), Group (roles, moderation, group encryption), Registry (discovery). An enclave is platform-blind (the host only sees ciphertext), portable (it is its keys plus signed history), composable (coordinate via signed commitments any third party can verify), and agent-compatible (indistinguishable from a person's). Discoverability is opt-in: list in a Registry to be found, or stay private.

Identity & lifecycle

An identity is a secp256k1 key with Schnorr (BIP-340) signatures, held by you — passkey, extension, or hardware, no phone number — never the server. The node is a single sequencer that orders writes, nothing more. Because the node only orders — it can't author or sign for you — its power is structurally bounded.

Authorization (RBAC)

Who may do what in an enclave is a small, decidable permission model baked into the verified kernel — three columns and six verbs, packed into a single bitmask so every check is one cheap, provably-correct computation, never a tangle of if statements.

Three columns — who you are:

• State (where you stand) — UPPER-CASE, mutually exclusive: PENDING, MEMBER, BLOCKED.
• Trait (your rank) — lower-case, stackable, each carrying a hierarchy: owner, admin, muted.
• Context (your relation) — Self, Sender, or Public, evaluated at check time.

Six operations — what you may do: Create, Read, Update, Delete, Push, Notify — permitted or refused by the columns. Deny is marked with a leading _, and deny always wins.

Authority changes are themselves signed events — Move (state, e.g. PENDING → MEMBER), Grant / Revoke / Transfer (traits), Gate (capability toggle), Shared / Own (key-value state) — each requiring explicit permission. A proven rank rule stops anyone acting on someone ranked above them.

Verifiable state & history

Current state commits to a Sparse Merkle Tree (one root); full history to an append-only Certificate-Transparency-style log; the two are bound and signed as a Signed Tree Head. Anyone verifies inclusion, append-only consistency, and any state fact offline, without trusting the node — history is tamper-evident. Optional validity proofs (zkEnc) prove state was reached only by authorized transitions, so a node can't write Mallory = admin and have a membership proof still pass. And privacy costs nothing here: an enclave's contents can stay encrypted while its state remains zk-provable — you can prove what's true about it without revealing what's in it.

Event sourcing and dataviews

Underneath, ENC is an event-sourcing store. Every change is an immutable, signed event appended to the log; current state (the SMT) is just a fold over those events. History is the database.

There are two ways to read it. A private app — a messenger, a DM, encrypted email — needs nothing else: the client holds the keys and queries the node directly for its enclave's events. Only when you need public, indexable data — a public timeline, a search index, an aggregate feed — does an (optional) dataview earn its place: a service that projects events into a queryable read-model and keeps it live. Delivery is part of the permission model: Push (P) streams full events to a dataview or service; Notify (N) sends a lightweight ping. A Registry is an enclave whose dataview indexes listings and serves them as a discovery API.

Write a signed event, read it back — querying the node directly for private data, or through a dataview for public, indexable data. On that foundation you can build anything — a private messenger, a public timeline, productivity apps, end-to-end-encrypted email, a headless agent API, or a category yet unnamed.

The mesh

ENC is not a central server and not a blockchain — a federated mesh of nodes. A node's role is deliberately narrow: it hosts enclaves, orders their writes, and delivers them — pushing events and notifications (the Push / Notify operations) to members and devices, holding data for offline sync and multi-device catch-up. It never authors writes or signs for you. Each enclave is ordered by one node, but that sequencer is bounded — it can't forge, reorder, or fake state — so you get edge-latency speed and one ordered source of truth without a central operator or consensus tax.

The network is ultra-flexible: a node runs anywhere — the edge, a server, your laptop, even your phone — and you can be your own node, so no third party sees your metadata. No lock-in, no censorship choke point, and your enclave survives any node dying — it just moves. An always-on node still gives reliable offline delivery and multi-device sync, keeping you sovereign without the peer-to-peer cost.

An enclave is a repository — keys plus signed history — so the tooling treats it like git for your data: you clone, push, pull, snapshot, and migrate it. Moving to another host or off one entirely is a single command, and snapshots round-trip byte-identically. Portability stops being a promise and becomes git clone.

IV. Privacy — transparent by default, private and pluggable

ENC is transparent by default — but transparent about the rules, not your content. State and every transition are verifiable and the log is tamper-evident, so anyone you allow can confirm that something happened and followed the rules; confidentiality layers on top, so the operator can store your data but never read it. The primitives are standard and conservative — secp256k1 with Schnorr (BIP-340) signatures, ECDH key agreement (Curve25519 / secp256k1), XChaCha20-Poly1305 authenticated encryption, and HKDF-SHA256 derivation. What's unusual is that which scheme protects a given piece of data is a swappable plugin, chosen by the conversation's shape:

• One party — your own private data — identity-aead: authenticated encryption under a key only you hold.
• Two parties — a direct message — dm-ratchet: a forward-secret double ratchet, so a compromised key doesn't expose past messages.
• A group — group-mls-lazy: a lazy variant of MLS (the IETF group-messaging standard) that scales it further — rekeying the whole group in O(log N) on a membership change while deferring the work lazily onto the enclave's real, verifiable history, so large groups stay cheap.

Crypto as swappable plugins

Each is a real package filling a typed slot — so you can swap or add schemes (post-quantum, a different group ratchet, a sealed-sender mode) without touching the verified core. Every plugin carries its own machine-checked security claim, so swapping never means "trust whoever wrote it": the guarantee travels with the plugin. Encrypted reads require an ECDH session, so confidentiality is built in, not bolted on. Privacy isn't a feature you're handed — it's a choice you own and can upgrade.

The subkey system — keys for agents and devices

You never hand an agent — or a new device — your root key. ENC issues subkeys: a subkey holds its own keypair, and your identity authorizes it with a co-signed certificate binding parent → subkey — both sides sign, so a verifier knows your identity authorized the subkey and the holder accepted it, all without your root key leaving your control. The certificate is time-boxed with an expiry, and subkeys rotate freely beneath your stable identity. A compromised agent or lost device has a bounded blast radius — read sessions are short-lived, access is revocable in real time at the membership layer (an RBAC Move/Revoke cuts a live feed mid-stream), the cert expires, and your root key stays safe. This is how a remote agent in the cloud or a local agent on your device can act as you under time-boxed, revocable authorization (§IX) — bounded by math, not a dashboard toggle.

V. One instance: a messenger

ENC is the substrate; a messenger is just one app on it — taken here because messaging is the hardest, most-contested consumer surface. Even there, the new paradigm shows: an ENC messenger owns your identity (no phone), your data (verifiable, portable), and your money — on a mesh no one controls. Every message is a typed, verifiable object that other apps and agents compose.

The table scores default, user-visible guarantees — optional modes, log retention, and network reach are separate dimensions.

Encryption is table stakes — ENC, Signal, WhatsApp, and Keet all have it. ENC does not claim to beat Signal on metadata — Signal trades privacy by storing nothing, the opposite bet from a verifiable, retained log. The rows where only ENC is green are the point: self-sovereignty, verifiability (formally verified — alone), and reliable delivery where pure-P2P Keet isn't. Network is reversed — the battle is distribution, not capability. This is only instance #1: the same AppGen machine produces the next thousand apps.

VI. Formal verification — trust, replaced by proof

The formalization gap

Every other "formally verified" protocol shares one unsolved problem: the proof covers a model, but the code that ships is hand-written — or now AI-written — and the compiler and runtime are trusted, not proven. A specification sits on one side, an implementation on the other; they drift the moment coding starts, and that gap is where bugs and backdoors live. This is the signature of the top-down method — theorize a spec, then hand-write code and hope it matches — which neither closes the gap nor keeps pace with the code machines emit. An audit only samples it — and no one can audit what no one fully read. ENC closes this gap.

Closing the gap by construction

ENC closes it by construction — and inverts the method. It formalizes the protocol from the behavior of real systems and drives that formalization as far up the proof as math allows — bottom-up, not top-down. The implementation is generated from the proven spec by a verified CodeGen: from one Lean 4 artifact — a small, closed, total calculus, EncDSL — four generators emit Lean, JavaScript (the SDKs and the Cloudflare host), Rust, and a Rust→WebAssembly kernel. No human hand-writes the protocol code; no AI writes it — the code is the spec, compiled. Because the generators are deterministic, a reproducibility gate regenerates every artifact and requires bytes to match hash-for-hash (sha-256) or the build fails. Key refinement properties are proven at the host boundary. So deployed bytes provably are the generated ones — there is no second codebase to drift. The same gate lets the protocol evolve safely: every new version is re-proven before it ships, never merely re-trusted.

The spec runs — its own reference

Here is what no other "verified" project has: the Lean spec isn't only a model on paper — it runs. Everyone else keeps a paper spec and a separate reference implementation, two artifacts that drift — the original formalization gap. ENC's spec compiles to an executable reference (the Lean enc-oracle), which decides every commit with the exact state machine the theorems are proved against. Validating the spec is validating the reference; there is no gap between them. Anyone can run that oracle as an independent referee to settle whether an event was valid, or who deviated in a dispute.

The proofs are the audit

The remaining links are closed concretely. The reproducibility gate regenerates every artifact and fails unless bytes match hash-for-hash. Generated tests (TestGen) replay the same workflow corpus across every platform through pluggable adapters, and a matrix theorem makes passing the two axes imply the whole grid. Witnesses run those tests against exact published bytes and record their hashes. Spec, proof, code, tests, and running bytes become one continuous, checkable chain — not a document and a hope.

SpecGen — created and audited

ENC isn't hand-built and hoped-correct; it's produced and graded by SpecGen, a protocol-agnostic framework that drives every claim along one pipeline: human-readable prose → a reviewed formal meaning → a Lean theorem → generated code → a witness that ran the real bytes → a single signed report. ENC is one instance of the SpecGen / CodeGen / AppGen / TestGen meta-protocols — generators that turn any domain into a fully-verified system. Aim them widely and you get a formally-verified, autonomously-evolving universe of software; ENC is simply its first citizen. The "audit" isn't a PDF from a firm that sampled code once — it's a machine-checked report that re-derives the entire chain and grades each claim.

Trust-minimization here is measured, not asserted: that report places every claim on a public trust lattice, from T0 ("trust the operator — nothing checked") up to T6 (a ratified, version-pinned release), with T5, proved & conformant, the tier where generated code provably matches the proof and witnesses agree. Almost no system can put a number on how much trust it removes; ENC can.

Verification all the way up

None of this is confined to the protocol kernel. Because the infrastructure and apps are generated from the same proven core, verification flows all the way up: you review a small declarative spec once, and math guarantees the expansion into a running, multi-platform app. That is the elegance — a tiny calculus that does the expanding for you — and what makes "formally verified" affordable for ordinary apps, not just a protocol.

It reaches infrastructure and scaling too — which is why ENC apps reach Telegram scale on a kernel small enough to verify. The proven kernel ships as a compact WebAssembly module on the edge: globally distributed and auto-scaling. Because the protocol is declarative and non-computing, work per event is tiny and bounded — verify, check the manifest, append, update the tree, nothing arbitrary to run. The node, policy layer, and host contract are all specified in Lean — even the server-side hook system is proven orthogonal (swapping hooks can't change replayed state). How it scales is proven, not just benchmarked: sharding provably preserves the full history (shards' union is the log), rebalancing loses nothing, shard assignment is bounded, and a connection-aggregating hub collapses socket overhead from O(clients × enclaves) to O(clients) + O(enclaves) — relaying frames verbatim as a metadata-only router. A Telegram-scale workload is mechanically modelled; raw throughput is measured, but correctness of scaling is proved — so the system grows without any guarantee quietly breaking.

VII. AppGen — redefining every app for agents

A verified core isn't safe on its own. The app is where your identity lives and where your agent acts — so an unverified app is a trusted black box between you and the proof, free to misuse the keys and permissions the protocol carefully bounds. Verifying only the node leaves the most dangerous layer unchecked: the app's behavior must be verified too. That's why, on ENC, apps are generated — emitted from the same proven core, so the parts that can hurt you (how it wields your identity, keys, and authorization) are verified by construction, not hand-written and hoped-safe.

Apps, generated not hand-built

An app is mostly declarative JSON — data types, mapping, actions, a UI tree — compiled by the Flow engine. Flow even resolves the infrastructure for you: it matches each piece of state to an enclave that can host it by its access model (who must read it back, how many parties, public or private), so you never hand-wire where data lives.

The interface isn't exempt from the math either. The ui-kit builds views from a formally-specified atom algebra — a closed set of UI atoms with composition laws — and its rendering implementation is proven to refine that algebra.

From that one definition ENC generates the typed SDK, the tests, native clients for ~10 platforms (built instantly by platform adaptors, not rewritten), and agent skills — so an agent drives the app through the same verified surface a human's SDK uses.

From a sentence of intent

AppGen goes the last mile: it turns a natural-language intent into a validated specification, then a generated, verified app — correctness proved once, reused across many. The generated apps are formally verified too — not hand-proved, but generated from a tiny reviewed spec through a proven pipeline. You review the sentence (tiny, human-scale); the math verifies the implementation. Cross-platform consistency is a theorem, so the same app behaves identically on all ~10 targets. Instant, ten platforms, verified.

Redefining the app landscape

The same machine that produces a verified, sovereign, agent-native messenger produces a marketplace, wallet, social feed, registry, payments app, identity app — each trust-minimized, owned by its users, and usable by agents, by construction. The ambition is not "a few apps on a new protocol." It is to redefine the existing app landscape for the agent era — every category re-expressed as a verified, composable, sovereign ENC app, generated rather than re-audited. AppGen draws on a corpus of reference apps and patterns to turn a sentence of intent into the next app instantly, with formally-verified security, across ~10 platforms.

Plugins & custom apps

Plugins make this extensible without bloating the proven core: the kernel encodes only what all apps share — the state machine and RBAC, generated and type-checked — and everything outside is a composable plugin filling a typed slot. Read-side projections (ranker, indexer, aggregator, filter), write-side gates (spam, moderation, fraud, validation), and the crypto suite (sign, verify, key-exchange, ratchet, group) are all slots; ~41 plugin packages fill the kernel-defined ones today. Each slot's type is its contract. You build custom apps the same generated way — spin up new enclaves, compose existing ones, or extend the verified SDKs, plugins, and UIs — and they inherit the proofs rather than re-earning trust. ENC provides the whole toolchain for exactly this.

VIII. Verifiable data → composability

Verifiability matters far beyond "was this message tampered with." Non-verifiable data is trapped in the conversation: a message, screenshot, or P2P chat record means something only to the people in the room. Hand it to a third party, another app, or an agent and it's a forgeable claim. Verifiable data is portable trust — it can leave the room and be checked by anything, without re-trusting the source. It stops being a dead end and becomes a building block.

Verifiability earns its place when data must be trusted by someone not in the room — money, agreements, cross-app inputs, an agent, or future-you after a reinstall. (Two people chatting don't need it.) Verifiability kills forgery, tampering, reordering, and deniability — it does not make content true. A verified object proves "X committed to this, unaltered, in order, and was allowed to" — which for money and agents is exactly what you need: can I hold them to it, and can anyone check?

Verifiable, not exposed

Verifiable does not mean exposed. With zero-knowledge proofs, data stays private while remaining verifiable — you can prove a balance is sufficient, a member is authorized, or a rule was followed without revealing the content. Privacy and verifiability aren't a trade-off; ZK delivers both.

So ENC isn't a verifiable messenger — it's a composable, verifiable data fabric.

IX. Built for agents

An agent has no human judgment to fall back on — so the trust a human supplied (reputation, a gut-check, support) must become something the machine can compute. The only computable trust is verification. Walk one transaction — your agent buys a service from a stranger's agent and pays — and every ENC primitive matters:

• Authenticity → the quote is signed; your agent can't be fed a forged or injected one.
• Bounded authority → your agent acts under a subkey authorized by a time-boxed, revocable certificate — your root key is never handed over and never exposed, even if your agent is buggy or hijacked. The authorization carries an expiry and can be revoked, so a compromise has a bounded blast radius and can never escalate into you. That's how delegating to an AI you don't fully trust becomes survivable — the leash is math, not hope.
• Verifiable receipts → the payment emits a proof the seller's agent checks before releasing. Agent-to-agent commerce is impossible without it.
• Ordered tamper-evidence → "deposit before release" is reliable.
• Mechanical disputes → a third party verifies the signed, ordered log and sees who deviated.
• Composability → the receipt feeds an accounting agent; the next agent verifies the last one's output without trusting it.

At every step, trust travels with the data, because two agents that share no central authority can't trust each other any other way. That's the gap between agents calling APIs inside one vendor's walls and an open agent economy where agents from different parties transact — and that wave is cresting now, with payment rails hitting exactly this wall.

Agent apps belong on ENC

So the framing flips: it isn't "agent apps need verifiability" — it's that agent apps should be built on ENC. On ENC, an agent gets the five things an autonomous actor actually needs:

• Identity — a sovereign, portable agent identity, with no central account to revoke.
• Memory — durable, portable, verifiable memory: its enclave is an append-only log it owns and can carry anywhere.
• Privacy — pluggable, formally-specified encryption over everything it holds.
• Composability — typed, verifiable data that other agents and apps consume as trusted input.
• Verifiability — every action is checkable, so trust travels with the data, not with a relationship.

Add RBAC-bounded delegation and a wallet, and any agent that can take responsibility should stand on ENC. "Agents are just regular users" is only safe because it's verifiable and bounded.

X. What you have to trust — minimized, and measured

The aim isn't zero trust — it's a trusted surface that is small, explicit, and measured: the soundness of the host platforms ENC runs on (the WebAssembly runtime, the browser, the edge), a few well-studied cryptographic primitives, and the integrity of code distribution. Everything above that line — that running code matches the proven spec, that history is intact, that state is valid, that your agent stayed in bounds — is backed by proofs you, or your agent, can check. The trust lattice puts a number on it.

That proof is empirical, not theorized — formalized upward from how real systems behave (§VI, §VII), not dreamed top-down and hoped into code. Replacing human audit with machine-checked proof doesn't just make iteration safe — it makes it fast: a proof checks in an instant where a human review would stall, so each new version is regenerated and re-proven before it ships, reproducibility-gated, advancing without anyone re-vouching by hand — safe because verified, not because someone signed off.

The human still owns what stays human-scale: the intent. You review the sentence; math owns the implementation, audit, and code that ships. This is the whole toolchain, not just the protocol: built by agents, for agents. Make the spec, proofs, code, and running bytes one continuous, checkable chain. Let your data leave the room carrying its own proof. Generate every app verified and sovereign. Prove, not promise, that the rules were followed.

The old paradigm trusted. The new one verifies. Own it — and prove it.