Formal specification (Lean)
CVN's load-bearing semantics — the dispatcher, the epoch ladder, and the
protocol rules under cvn/enc — are specified in Lean in impl-spec
(spec-lean/Enc/Cvn/), as executable definitions with theorems checked by
Lean's kernel, and the TypeScript is held to them by a conformance corpus the
model itself emits.
What is proved
Enc.Cvn.Dispatch — the dispatcher:
| theorem | says |
|---|---|
performNow_never_drops | a Cmd is performed or refused — there is no third outcome |
refusal_names_kind | a refusal names the kind it could not route |
run_records | while recording, running an action appends exactly its emitted Cmds and performs nothing |
dispatch_performs_all_in_order | outside a dispatch, every emitted Cmd — nested dispatches included — is performed exactly once, in emission order, after the action, and the recording closes |
nested_dispatch_drains_nothing | a nested dispatch appends to the outer list and drains nothing |
perform_outside_is_immediate | outside any dispatch, perform performs now |
dispatch_performs_exactly_emitted | nothing invented, nothing lost |
Enc.Cvn.Ladder — the epoch ladder (shared/kernel/dm-epoch.ts):
| theorem | says |
|---|---|
replay_is_idempotent | identical bytes at a held epoch: silent, unchanged |
conflict_is_refused | different bytes at a held epoch: refused |
refused_leaves_ladder | a refusal never changes the ladder |
opens_at_zero | an empty ladder accepts exactly epoch 0 |
accepted_is_above_max | acceptance is strictly monotone |
accepted_is_held | what was accepted is held afterwards, with the bytes given |
Enc.Cvn.Inclusion, Enc.Cvn.DmWire, Enc.Cvn.DataView — the protocol
rules under cvn/enc; the theorems are listed there beside each
module. The ones that are properties rather than examples:
| theorem | says |
|---|---|
inclusion_ok_iff_all | an event is in the log exactly when all three checks hold |
messageTags_head | a DM message's first tag is to, always |
DataView.step_le_maxSubs | whatever the frames, a socket never holds more than 32 subs |
DataView.query_ends_with_eose | an accepted query's last frame is EOSE |
DataView.broadcast_delete_all | a delete reaches every sub on its table, matched or not |
DataView.upsert_present | a strictly newest upsert survives any positive cap |
DataView.diffKeys_disjoint | a key is never both started and stopped |
InviteNotice.toSealed_valid | every notice the app builds satisfies the spec's rule: a handoff carries its epoch number |
InviteNotice.select_never_zero | the mint secret is never handed off |
Identity.push_before_commit | the DataView push goes before the enclave commit |
Identity.unpushed_not_stamped | a row that committed but never reached the DataView is not published, and the next attempt sends it again |
Submit.outcome_refusal_keeps_sent | a refused sent keeps its optimistic row: the WS echo owns that verdict |
Submit.enqueue_length | an id is never queued twice |
Query.length_le_1000 | a node never returns more than 1000 events to one query |
Query.sorted_when_reverse | with reverse, the result is newest first |
GroupWire.kick_excludes_target | a removed member never receives the epoch that follows its removal |
GroupWire.admit_wider_than_spec | the app rotates on BLOCKED→MEMBER, which the spec's epoch rule does not name |
RbacWire.transfers_dropped | the transfers section never reaches the node: ownership transfer is unreachable on this wire |
RbacWire.no_outsider_key | nobody is enrolled as an outsider |
Push.backoff_uncapped_diverges | at the ninth retry the node waits 512 s where the spec caps at 300 s |
Push.tags_default_empty | an event with no tags is stored with [], never null |
Signaling.echo_never_to_sender | an echo never returns to the socket that sent it |
Signaling.read_monotonic | a read cursor never moves backwards |
How the code is held to it
The DSL that impl-spec compiles to TypeScript is first-order (bytes, maps,
scalars, crypto); a dispatcher with callbacks is not expressible in it, so the
TypeScript stays hand-written and is refined by replay, the same way the
wire protocol is held to enc-oracle:
lake exe cvn-oracle(inimpl-spec/spec-lean) runs the Lean definitions over a fixed corpus and writesspec/cvn-conformance.jsonlinto this repo — one JSON line per case with the model's expected outcome.test/spec-conformance.test.mjsreplays every dispatch case throughcreateDispatcher;impl-super-mvp'sladder-conformance.test.mjsreplays every ladder case throughdmEpochSet;test/enc-*.test.mjsreplay the inclusion, dm-wire and dataview cases throughcvn/enc, andimpl-super-mvp'sdataview-conformance.test.mjsreplays the dataview cases through the real server module and kernel.spec/codegen-manifest.jsonpins the corpus by SHA-256;test/manifest.test.mjsrefuses a mismatch — a model change that was not re-generated, or a corpus edited by hand.
What this proves: the implementation agrees with the model on every case the
model enumerates. What it does not: that the corpus covers every path — a
new behaviour gets a new case in Enc/Cvn/Oracle.lean, and a new theorem when
it is a property rather than an example.
What is formalized, and what is not yet
A rule counts as formalized only when all three hold: Lean states it and its
theorems check, the oracle emits its cases, and the real code replays
them — the module the app ships, not a copy. impl-super-mvp's port plan
(CVM-PORT-6.md) names, per verb family, the protocol residue the family
surfaced. Its state on 2026-09-18:
| residue | family | state |
|---|---|---|
| the epoch ladder | dm | Enc.Cvn.Ladder, replayed through dmEpochSet |
| verify-event (inclusion) | explorer | Enc.Cvn.Inclusion, replayed |
the DM envelope, its tags, epoch 0, the r-tagged Delete and Update | dm, submit, message-ops | Enc.Cvn.DmWire, replayed |
| the subscription diff, the DataView frames, the server's step | subscriptions | Enc.Cvn.DataView, replayed three ways |
| the invite-notice envelope and handoff | invite | Enc.Cvn.InviteNotice (refines Enclaves.Personal), replayed through the real kernel module |
| the profile-publish event, the registry keys | profile, lookup | Enc.Cvn.Identity (refines Registry.RegIdentityContent), replayed through the real publisher, families and registry DO |
| the submit command and its receipt | submit | Enc.Cvn.Submit (refines NodeAPI), replayed through the real kernel modules |
| query-enclave-events | explorer | Enc.Cvn.Query (beside Handlers.QueryFilter), replayed through the real adapter and node |
| the membership Move | group | Enc.Cvn.GroupWire (refines Enclaves.Group), replayed through the real roster, readmission and enrichWelcome |
| the mint manifest and initial state | mint | Enc.Cvn.RbacWire (the wire manifest Manifest.lean does not model), the shell and the protocol tier through one source |
| the DataView push envelope | moments | Enc.Cvn.Push (beside Enc.Core.Push, what ships), replayed through the real client, node pipeline and DataView DO |
| signaling frames | calls | Enc.Cvn.Signaling (new: the spec assigns the relay to the host), replayed through the real SignalHub |
The column is closed. Where the spec already defined the shape, the
Enc.Cvn module imports and refines it and its header lists what the app
carries that the spec does not; where the spec had no shape — the wire
manifest, the relay — the module states what ships. What the survey found
along the way and this work reports rather than changes, filed upstream on
2026-09-18 with the exact lines: the generated core's event-hash domain
(computeEventHash inlines 1 where Event.lean pins 0x11 —
impl-spec #19),
signCommit ignoring its alg argument
(impl-spec #20),
Enc.Core.Push disagreeing with the node's shipped pipeline
(impl-spec #21),
STHResponse's swapped t/ts
(impl-node #12),
and the wire manifest with no place for gates, aliases, scoped grants,
transfers and retention
(impl-node #13).
Two are the app's own and are fixed in the families that own them, each
with its replay case first: the registry's /reg_enclaves and /reg_nodes
routes it does not serve (lookup), and the cursorless first WS connect
against decideReplay (subscriptions).
The app's own decisions are modelled too
The column above is ENC's. It was written when the app's own decisions — the 87 invariants across sixteen families — were held to be sentences a test refutes, not theorems, on the reasoning that they name Super's nouns and Lean would prove Super rather than ENC.
That turned out to be the wrong line, and it was moved. A family's decisions are exactly the kind of thing a model is good at — which enclave a write names, which cipher seals it, what a receipt does to the row it was for — and the reason to model them is not proof for its own sake but the corpus: a decision with a model has cases, and cases replay through the shipping module. Every family that has a run has one:
| family | model | theorems | cases | what it states |
|---|---|---|---|---|
| submit | Families.Submit | 63 | 103 | which enclave a write NAMES, which of five ciphers seals it, the epoch-zero ask, the three manifest grants a delete routes by, what a receipt does to its row |
| dm | Families.Dm | 39 | 56 | the plaintext refusal's three shapes, the peer route, the retry fallback, the mirror's tags, and the three ways a message skips the ratchet |
| lookup | Families.Lookup | 34 | 41 | who a key belongs to, the cache, the bounded re-ask |
| pay | Families.Pay | 26 | 32 | the asset and its decimals, the refusal, the faucet plan |
| persist | Families.Persist | 23 | 34 | the key templates, the value serialisation, the active-enclave pair |
| message-ops | Families.MessageOps | 22 | 19 | one composer in two moods, the truncations, forwarding's provenance |
| moments | Families.Moments | 21 | 27 | what a retraction IS, and the tombstone that comes first |
| mint | Families.Mint | 20 | 25 | the mint's chain, the setup, the admits one at a time |
| group | Families.Group | 18 | 27 | membership as a FOLD over the log, which is what refuses the resurrection |
| invite | Families.Invite | 17 | 20 | the picked members, the banner, the self refusal |
| agent | Families.Agent | 16 | 13 | the install, and why a missing provider answers OK |
| explorer | Families.Explorer | 15 | 17 | the tree head, the events, the inclusion proof |
| profile | Families.Profile | 11 | 12 | the publish, and what it carries |
calls, open and subscriptions declare NO_RUN and decide nothing, so
there is nothing to model — and clean/test-port-complete.mjs knows the
difference: it derives Families/<Name>.lean from the family name and refuses
a family with a run and no model, no corpus kind, or a replay that does not
import the module it claims to replay.
Two of these models went in stating a type the code does not have — a
Staged { replyArmed, editArmed } record in message-ops, and a
isMembershipChange written as a list of two events the app never emits.
Both were true theorems about a fiction; both were caught by the replay,
which is the only thing that can catch them.
Regenerating
cd ../impl-spec/spec-lean
lake build Enc # the proofs (Enc.Cvn.* are in the library)
lake exe cvn-oracle # the corpus → ../impl-cvn/spec/then update expectedDigest in spec/codegen-manifest.json to the new
SHA-256 and commit both repos. Enc.Cvn is part of EncProofs, the
framework-free public verification surface, so a public clone re-checks these
theorems with the codegen framework absent.