How acceptance works

What happens between a draft and an accepted object, what the kernel replay checks, and why every native call runs in a sandbox.

An object in a Lema store is accepted when it is stored with a kernel receipt, or when it is checked through a declaration that has one. Everything before that is a draft. The sections below follow a draft through submit. For the commands, see the first-proof tutorial and the server methods reference.

Untrusted drafts

elaborate takes restricted Lean, plus Received.* bindings to objects the store has already accepted, and returns a draft. A draft is a set of canonical objects that is not stored. To build it, the server runs Lean’s elaborator on the author’s source, with its tactics and macros. Then the exporter (lean/codebase/Exporter.lean) turns the elaborated declarations into objects. None of that is trusted. The elaborator is large, and the source it runs was written by an agent.

submit is what accepts. It takes a draft and replays its closure through the pinned Lean 4.34.1 kernel, and the closure is accepted whole or not at all. publish is elaborate followed by submit inside the server, so a client never has to hold a large draft. A draft from anywhere else, such as another store’s export or a hand-edited file, goes through the same replay and passes or fails on the same terms. (import is submit under another name.)

Lean itself is built the same way: the elaborator produces terms, and a small kernel re-checks them. Lema keeps that split across a process boundary, and the source text is not part of what the kernel sees.

What submit checks

Before any native call, the Rust side validates every object against the identity rules and computes the closure. It refuses anything that nothing in the submission would check, such as a proof that no declaration uses. Stale alias expectations are refused at this stage too, so these refusals cost no kernel time.

Next, the closure’s new declarations are written as a replay payload, replay.jsonl (schema lema.replay/v4), with one declaration per line under the kernel name LemaStored.h<id>. The decoder (lean/codebase/Decoder.lean) runs in the pinned Lean, reads the payload one line at a time, and:

• checks that the namespace’s Lean version and githash equal the running Lean’s;
• rebuilds each declaration and adds it with the kernel’s addDeclCore, never installing a constant directly;
• compares regenerated family helpers, and the proof marking of each value, with the stored rows;
• refuses any installed constant that cites something other than a stored constant or a listed Init external;
• computes each constant’s axiom footprint with collectAxioms.

The kernel’s verdict is read only from a file the decoder writes at the kernel boundary. Log text can echo strings from the draft, so it is never read for the verdict. If the kernel runs out of time or memory, the result is inconclusive, and nothing is accepted.

The footprints then go through the axiom audit. A fixed floor is always refused, whatever the store’s policy says: sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, any axiom with a _native name component (what native_decide adds) and any unsafe constant. Above the floor, the footprint must be within the store’s axiom policy. The policy is set when the store is created, and no command changes it. The default is Lean’s standard axioms, propext, Quot.sound and Classical.choice (decision 0028), and lema init --axioms propext,Quot.sound creates a narrower store.

If everything passes, the store writes receipts. Declarations, records, families and externals get one each. Statements, templates, proofs, satisfactions and the namespace object get none, because their footprint depends on how they are bound. Each of them is accepted through a declaration of the closure that uses it directly, and the store records which one (checked_through).

A receipt names the object, the checker, the axiom footprint, the module that holds the declaration, and the call. The checker entry gives the Lean version and githash, the target, and hashes of the Lean binary, the distribution and the pinned host files. Receipts are local. A store does not take another store’s receipts, so objects that move between stores are replayed again.

Incremental replay and the module cache

Replaying a whole closure on every submission does not scale. Before incremental replay, every submission re-checked its entire closure, capped at 4,096 declarations and a per-call time budget. A standard library with applications on top would have exceeded that.

So each accepted delta becomes a Lean module, LemaDelta.d<hash>, that imports the modules of its dependencies. A later submission imports those modules, and the kernel checks only the new declarations. In the reuse run of 16 Oct 2026, a consumer of twice_id replayed one declaration, its own, and imported the module holding twice_id.

This rests on the module cache’s trust assumption. Lean does not re-check imported declarations, and it reads their axioms from the module’s recorded table. The rules around the cache keep that assumption narrow:

• a module counts only if the pinned checker wrote it after a replay, and only while it still has the hash recorded in the cache index;
• every module is re-hashed before it is loaded;
• the cache is keyed by the Lean tooling, the Rust translation from objects to kernel declarations, and the toolchain, so a change to any of them starts a fresh cache.

Stores that share a runtime output share its cache. A store that reuses a module reuses its receipts after checking them against its own policy and the floor.

Re-checking from scratch

reverify removes the module-cache assumption for what it covers. It replays every accepted object, or the closure of the roots it is given, from scratch and with no imported modules. It compares each fresh footprint with the stored receipt, and requires every other object to be used by a declaration replayed in the same call. Any difference is an error. One call covers at most 20,000 objects, so a larger store is re-checked in parts. See Re-check a store from scratch.

The sandboxed runtime

Every native call that elaborates, replays or compiles runs under the pinned Linux runtime in crates/lema-check:

• the pinned Lean 4.34.1 distribution, with every file hashed against the reviewed manifest when the runtime loads, and a metadata snapshot of it compared before and after each call;
• bubblewrap, with a new session and no shared namespaces (so no network), the system and toolchain read-only, and only a fresh work directory writable;
• a transient systemd user scope with 4 GiB of memory, no swap, 32 tasks, one CPU and a runtime ceiling;
• a supervisor that enforces wall time, caps the log at 16 MiB, cleans up the process group and confirms the scope is gone;
• a host lock held for the whole call, and a preflight that, among other checks, requires at least 6 GiB of available memory;
• a ledger, ledger.jsonl in the runtime output, with a reservation before each call and a completion after it.

Any supervision fault writes a HALTED latch. It is HALTED in the output directory, or a host-wide latch beside the shared lock when the scope could not be cleaned up. Every later native call is refused until an operator resolves it (Recover from a HALTED latch). Capability applications run under the same controls in a profile that shares the host’s network. Checker calls never use that profile (How programs reach the outside world).

The runtime exists because elaboration runs author-supplied Lean, and the kernel can be given unbounded work. The limits keep a runaway call from taking the host down. The ledger accounts for every native call, so a reservation with no completion is visible. The latch exists because a call whose cleanup could not be confirmed leaves the host in an unknown state, and the runtime stops rather than guess.

What acceptance covers

An accepted object is checked: kernel replay accepted it, within the store’s axiom policy above the fixed floor. Until reverify replays it from scratch, that also rests on the module cache’s assumption. Acceptance does not say that a contract states what you meant. It says nothing about compiled code either; the behaviour of compiled code is tested. The kernel itself, the decoder that turns objects into kernel declarations, and the reviewed Rust acceptance path (lema-core, lema-check, lema-store) are assumed. Checked, tested and assumed covers the three labels, and the trusted base reference lists every assumption.