Checked, tested and assumed

What the three evidence words mean in Lema, why they are kept apart, and what no claim covers.

Every claim Lema makes about a program names the kind of evidence behind it. Take SHA-256. The theorem digest_abc in lean/std/Sha256Spec.lean says that the specification’s digest of the three bytes abc is NIST’s published answer. The pinned Lean 4.34.1 kernel evaluated it, and the store accepted it. Separately, the execution manifest lean/exec/sha256-vectors.json runs the compiled code on the same vectors under two backends and compares the output byte for byte. Neither of these says that the C compiler that built the second executable is correct, or that Linux ran it faithfully. Nothing in Lema says that. These are three different statements, and Lema has a separate word for each.

Three words

“Accepted” is narrow too. It means an object stored with a kernel receipt, or accepted through a declaration of its closure that has one (checked_through). The docs avoid “verified” on its own, because it does not say which kind of evidence is meant, and a test is not called a proof.

What each word covers

Checked

A checked theorem holds for every input its statement quantifies over, given the axioms in its footprint. The server gets there by source-free kernel replay. It turns the canonical objects of a closure back into kernel declarations, re-adds each one with addDeclCore, and reads the axiom footprint Lean collects for every constant. The footprint must stay above the fixed floor: no sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, _native axioms or unsafe constants. It must also stay within the store’s axiom policy, which for a new store is propext, Quot.sound and Classical.choice. How acceptance works describes the steps.

Two qualifications travel with the word. First, replay is incremental, and Lean does not re-check the modules that earlier replays wrote. Between full runs, “checked” also rests on the module cache’s integrity, and lema reverify replays everything accepted from scratch, without modules. Second, a Lean file that the pinned Lean elaborates on a developer’s machine is “checked locally”, which is not acceptance. The merge gate claims “tested” or “checked locally”, never “accepted” (decision 0033). lean/core/Transport.lean and Protected.lean are in that state: checked locally, with their store acceptance test written but not yet run.

Tested

A test runs something and observes what happened. Tests cover what no proof in Lema reaches: that compiled code prints the bytes the model predicts, that a shim refuses an unapproved origin, that an atomic write survives a kill, that the store refuses a stale alias move. A test samples. It says that these inputs, on this host, with this toolchain, gave this output.

The docs also say where a test ran. Many recent store features are “tested without a runtime”. Their rules run in cargo tests over placeholder receipts, while the native suites that would run them against the pinned runtime are written but not yet run.

Builds connect the two kinds of evidence without merging them. An execution manifest names its roots by accepted ID. lema build refuses unless the roots compile to exactly those IDs and their closure is the accepted closure. So the running code is bound to the proved objects by identity, but its output is still only tested. The artifact’s manifest says so in its claim field (“no proof receipt or compiler correctness claim”), and the claim in a lema test report ends “nothing here is a proof”.

Assumed

Some components are trusted without proof. The main ones are:

• the Lean kernel and compiler, and the reviewed Rust acceptance path (lema-core, lema-check, lema-store), including canonical validation and the decoder that turns canonical objects into kernel declarations;
• glibc, Linux and the local operator;
• for native builds, leanc, clang, ld.lld and the Lean runtime, and for a standalone build, that the emitted C is the compared Lean.IR’s;
• for capability applications, rustls, ring, webpki-roots, the resolver, the network and Lean’s task manager.

The trusted base reference lists them in full.

Why the words stay apart

The three kinds of evidence fail in different ways, and they are re-established in different ways. A theorem’s acceptance does not depend on the machine that later runs the code, and reverify can re-establish it from scratch at any time. A test result is tied to a toolchain, a host and the inputs it tried, and says nothing about other inputs. An assumption is only as good as the component’s own record. If one word covered all three, a reader could not tell which of them they were relying on.

Decision 0031 applies this to applications. Theorems about Lema programs over their capability models are checked. That the binary realises them rests on the tested and assumed parts.

The retired HTTP/1.1 health and echo service in lean/http used all three words for one program. Its HealthEchoV1 guarantee was checked for two parser representations. Its compiled artifact was tested: 3,348 parser and oracle comparisons, 28 driver scenarios, a socket smoke test, and 34 malformed, incomplete, limit, reset and timeout connections for each parser. Its compiler, sockets and operating system were assumed. Decision 0033 retired that chain. It is still in the tree at commit 5a94951, but it is not current work.

How the tools show evidence

lema site build writes static pages that give every declaration three separate panels, never one badge:

• proof acceptance (Std.Guarantee.Proof): the kernel receipt with the actual axiom footprint, and the store’s policy shown apart as the ceiling;
• specification review: the review records that bind the declaration;
• execution and IR evidence (Std.Guarantee.IR, leanc): guarantee records from the IR profiles, and the releases whose closure holds the declaration.

The labels are the same words, checked, tested and assumed, plus a fourth, reviewed, which the pages gloss as “a decision, not a proof”. A contract view carries a label of its own: “structural round trip: same identity”, “unsupported rendering” or “does not round-trip”. The generator is tested on a synthetic store with placeholder receipts, and its native test has not been run. Build static inspection pages shows how to produce the pages.

A release adds no claim. Its proof receipts are the store’s kernel receipts (checked). Its artifact, IR receipts and capability platform are tested, and the compilers, runtime and OS are assumed. Pinning them together in one record makes a deployment reproducible. It does not make any part of the claim stronger.

Reviewed means that an actor with review authority under a project reference’s policy approved a transition. The review record binds what was approved: the declarations, their closure, the policy and its version, and optionally the exact text displayed. The authority (delegated or steward) is what the policy grants that actor. It is not evidence of who the actor is. A review records who approved a contract. It does not show that the contract captures the intended requirement. Agent review of the project’s own code is technical review, not human assurance.

What no proof covers

A contract only guarantees what it states. The kernel checks that a proof fits its statement. Whether the statement is complete enough for its use is a human judgement, which is why contracts are kept small enough to read. A proved property can also be narrower than it sounds: functional correctness of SHA-256 is not collision resistance, which stays an assumption.

Contracts state behaviour, not cost. A checked replacement says that a safe client gets the same results from two implementations. It says nothing about speed, memory use or timing side channels, and a correct replacement could be 1,000 times slower or leak a key through timing. Lema makes no claim about running time unless a model states one. lean/core/Fueled.lean bounds the work in each slice of a fueled program in declared cost units (slices_le_gap, checked locally). How those units become time is tested or assumed.