ENC Protocol — Spec

The normative protocol spec, divided by dependency layer. The kernel holds the protocol math and canonical semantics; the node realizes it at runtime; and the app layer — enclave profiles and confidentiality plugins — builds on top.

Verify it yourself — the live spec dashboard

spec.enc.md is the verifiable-spec dashboard: a single static page that lets anyone re-derive every number from one clone — no trust required. It contains:

The verification method — the exact, copy-pasteable recipe: git clone … && lake build EncProofs to kernel-check every theorem, #print axioms to bound the trust base (no hidden sorry), regenerate all code from the spec, and sha256sum it against the attested digests so the deployed code is the proven code.
Every theorem — all 2,605 machine-checked theorems, searchable, each with its Lean module.
The trust base — the 81 declared cryptographic axioms the proofs rest on (the complete, declared assumption set).
The claims ledger — 1,568 normative spec claims, each bound to the Lean theorem that proves it.
Attested artifacts — every generated artifact with its location and sha256 digest, under one BIP-340-signed attestation.

It's fully self-contained and offline-verifiable — the dashboard only displays numbers you can re-derive yourself.

Kernel

Protocol math and canonical semantics.

Protocol summary — trust model, core abstractions, cryptography, wire protocol, event semantics, lifecycle
RBAC — RBAC v2, contexts, manifests, authorization, per-event processing
Sparse Merkle Tree — state and proof semantics
Certificate Transparency — log and proof bundles

Node

Node, server, and runtime behavior that realizes the kernel.

Node API — REST / WS / session / errors, hooks, DataView surfaces
Migration — migration modes, checkpoints, backup / restore
ZK validity proofs — zero-knowledge folded validity proofs

Enclaves

The enclave profile catalog and per-profile semantics.

Plugins

Confidentiality plugins and the cryptographic suite registry.