Re-check a store from scratch

Replay accepted objects with the pinned Lean kernel and no cached modules, and compare every axiom footprint with its receipt.

Normal acceptance is incremental: later replays import cached modules, so the pinned Lean 4.34.1 kernel checks only new objects, and the earlier ones rest on the module cache (How acceptance works). reverify replays objects from scratch, with no modules, so the objects it replays no longer depend on that cache.

Before you start

• A running server on the store, with a runtime that can make native calls: no HALTED latch, and a quiet host.
• In the commands, $SOCK is the server’s socket.

Steps

1. Check how many objects the store has accepted:

   lema --socket $SOCK info

   One reverify call replays at most 20,000 objects. If accepted is larger, go to step 3.

2. Re-check everything:

   lema --socket $SOCK reverify

   This is one native call. The response is {call, notes, objects, receipts}:

   • objects: how many objects were re-checked;
   • receipts: how many kernel receipts the replay produced (for declarations, records, families and externals);
   • notes: how many other objects were covered by a declaration replayed in the same call;
   • call: the native call’s name in the runtime’s ledger.

3. For a larger store, re-check it in parts. Pass roots, and the call replays their closure:

   lema --socket $SOCK call reverify --params '{"roots": ["<id>", "<id>"]}'

   Choose roots whose closures together cover every accepted object. The lean/cap publication suite, for example, re-checks its store in three parts, each the closure of some publications’ roots, and checks that together they cover every accepted object.

Reading the result

A pass means two things. Every receipt’s axiom footprint equals the one worked out now. Every object without a receipt (a statement, template, proof or satisfaction) is used directly by a declaration replayed in that call. Any difference is an error.

Time and size

One call may run for at most 600 seconds, and the 20,000-object bound is meant to keep a call within that. In the lean/cap publication run of 17 Oct 2026, parts of 16,926, 13,066 and 15,430 objects took 63, 156 and 54 seconds (lean/cap/README.md).

A call that runs past its limit is a supervision fault: it writes a HALTED latch and stops later native calls. Split the store into smaller parts rather than let a call run long.

Refusals