Component · spec & evidence

Certificate Kernel Execution Lab

Runs the Lean verifier over a small public proof project and reports which rows it accepted.

Contract

Does It builds a small public Lean/Lake project, then runs the Lean verifier over declared "transition" rows that reference a set of generated "certificate" declarations, and writes a structured result record showing which rows the verifier accepted, which it left unresolved or rejected, plus the exact build command, return code, and file hashes. The result record is honest, inspectable evidence that a real Lean verifier ran on public material, with proof text, provider/oracle output, and private source deliberately excluded from the result record and that exclusion recorded (not silently dropped) rather than passed off as evidence.

Scope limit It is a local tool-witness that the declared public fixture rows compiled and were adjudicated by the local Lean verifier; it excludes general proof authority, count oracle/provider output as proof, expose proof text, change source files, claim a benchmark solve-rate, or include launch operations.

Run

microcosm certificate-kernel-execution-lab run --input fixtures/first_wave/certificate_kernel_execution_lab/input --out receipts/first_wave/certificate_kernel_execution_lab

Evidence

ClassExternal tool runevidence 4/5Real runtime resultRuns real tools

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module