Trusted base

What Lema checks with the kernel, what it tests by running, what it assumes without proof, and what it does not claim.

Lema labels evidence with three words. This page lists what each one covers, as docs/architecture.md (“Trust boundaries”) and docs/roadmap.md (§13, “Not claimed”) state it. Checked, tested and assumed explains why the three are kept apart.

Checked

Kernel replay of the objects, within the store’s axiom policy above the fixed floor, under the module cache’s assumption: Lean does not re-check imported modules and reads their axioms from each module’s recorded table. lema reverify checks from scratch, without modules.

A Lean file that the pinned Lean elaborates outside a store is checked locally, not accepted. The merge gate (decision 0033) claims “tested” or “checked locally”, never “accepted”.

Tested

• compilation;
• the worker runner and loopback service (the HTTP v1 execution chain, retired under decision 0033);
• OS behaviour;
• the output of an execution manifest’s program (lema run, lema test);
• the capability applications’ runner (lean/cap/Runner.lean) and shims (crates/lema-cap), at their boundary;
• the project-reference rules and their actor check, a local bearer-token comparison that separates cooperating actors but not the store’s own OS user.

The executable vocabulary, the startup check and the IR profiles read an inventory from the process that elaborated the source, so they guard against honest mistakes, not a hostile draft. No proof receipt is issued for executed output.

Assumed

Receipts are store-local and never trusted from another store: objects moved between stores are replayed again (decision 0027).

Not claimed

docs/roadmap.md §13 claims no:

• proof of the Lean compiler, the Rust code generator (the Rust backend, on hold under decision 0029), rustc, tokio, the OS or network delivery;
• public foundation or production assurance;
• human-qualified review.

Two limits follow from the model itself. A contract guarantees only what it states, and a review record says who approved a statement under which authority, not that the statement captures the intended requirement. Contracts state behaviour, not cost.