Component · spec & evidence

Verifier Lab Execution Spine

Runs Lean on small bounded proof attempts in a temp copy and records what passed or failed.

Contract

Does It copies a small public Lean math project into a throwaway temporary workspace and actually runs the Lean/Lake checker on a handful of small, bounded proof-step attempts the tool builds itself. It then writes down what the checker said: which attempts were accepted, which failed, and the failure category for each, plus safety counts (for example, how many attempts tried to sneak in forbidden content and were rejected). The pass/fail facts and the safety counts are readable directly, while the tool never shows the underlying proof text, never calls any outside service, and never modifies the original project or any existing source files.

Scope limit It is a tool-witness result record for bounded public Lean transition rows only: it does not establish general proof authority, count oracle/provider output as proof, export proof bodies or tactic scripts, use external model services, change source files, claim benchmark solve-rates, or include launch operations/public sharing.

Run

PYTHONPATH=src python3 -m microcosm_core.organs.verifier_lab_execution_spine run --input fixtures/first_wave/verifier_lab_execution_spine/input --out .microcosm/verifier_lab_execution_spine

Evidence

ClassExternal tool runevidence 4/5Real runtime resultRuns real tools

Links to Certificate Kernel Execution Lab, Engine Room Demo

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module