Architecture

Every change is a signed request. The Lean kernel admits it, leaving a receipt, or refuses it with a reason.

Admission

The kernel checks a request against current capabilities, laws, exact read roots and funding, and checks a computation by running it again, at admission and on every replay. No admission uses a proof. The proof-system research, Selvage, is outside the deployed build except twelve modules behind the Host's digest backend.

A signed invocation of an Objective method is admitted the same way. The receiver re-runs the Lean front end on the published package and admits only a core equal to its own output, requires the claim's declared envelope to be priced by one public tariff, runs the method, and requires the Plan's effects to equal the command's. This ran on scratch worlds (journey row objective); it is not deployed.

Grants and laws

An owner delegates a grant with named verbs and can revoke it. Each resource has a law, a predicate checked on every change. A law that denies everything is permanent:

mini> law lock notes {"type":"any","predicates":[]} --allow-unsatisfiable
mini> submit lock
mini> read notes
# refused: law-denied: sealed
mini> law unlock notes {"type":"all","predicates":[]}
# refused: law-denied

Receipts and retries

A receipt names the transaction, the resulting world root and a confirmation such as installed or replayed. A refusal names one of fourteen reasons, such as no-grant, law-denied or stale-root. A lost reply is answered by looking up the same call bytes, never by a new request; a retry returns the same receipt.

Consent

The SDK (Rust, and TypeScript byte-identical to it) runs on the member's device and does not trust the operator. Before a key signs, a Lean consent process the member chose re-derives the plan and returns the exact header bytes that key may sign; the SDK signs nothing else. A browser has no consent process, so until a bridge to a member-held replica exists, a browser must not sign.

Private rooms

Main only; devnet quality; privacy not audited. A member's words are sealed on their own machine under the room key, which the node holds only wrapped to each member (X25519 + ML-KEM-768). The node still sees who is in the room, who wrote when, and line sizes in 64-byte steps. The founder key is trusted on first use.

Agreement

A Generic Simplex BFT engine, written in Lean and compiled native, for n = 3f + 1 replicas with at most f Byzantine. Safety is proved over the Lean engine model. Liveness is not established; the executed run was four replicas on one host.