Certificate Kernel Execution Lab

Lab answers question

The lab answers one question: did a real Lean verifier just compile a small public project and accept the declared certificate rows, with the command, return code, and hashes recorded. The certificate kernel execution lab answers one narrow question. Did a real Lean verifier compile a small public project and accept the declared certificate rows, here and now, with the exact build command, the return code, and the source hashes on record? Everything else the component produces is bookkeeping that keeps that answer honest.

Runs lean project

It runs the Lean project in a temporary copy, checks rows against a decidable Boolean checker, and writes a metadata-only record of accepted, residual, and rejected rows with command and hashes. It runs a source-available Lean/Lake project inside a temporary copy, checks generated certificate rows against a decidable Boolean checker, and writes a structured result record. The record names which rows the verifier accepted, which it left unresolved, and which it rejected, together with the build command identity and the file hashes. Proof text, provider output, and private source stay out of the record, and that exclusion is written down rather than dropped in silence.

Both public entrypoints, run and run_certificate_bundle, build one payload through _build_result and write it as metadata-only public evidence. The public entrypoints are run and run_certificate_bundle in src/microcosm_core/organs/certificate_kernel_execution_lab.py. Both build one payload through _build_result and write it as metadata-only public evidence.

Purpose

Facts as finite certificate plus decidable checker

Proof-adjacent facts become a finite certificate plus a decidable validate : Cert -> Bool checker, so the agent supplies rows and Lean decides across two checker families. A large class of proof-adjacent facts can be written as a finite certificate plus a decidable checker shaped like validate : Cert -> Bool. The component never asks an agent to write a human proof. It asks for the right certificate rows and lets Lean decide. The fixture carries two checker families, NatSumCertificate over arithmetic and BoundedOrderCertificate over a bounded modular order, so sign-off is not one hard-coded shape.

Sign-off needs exit-zero Lean, not a screenshot

A row counts as accepted only when the runner shells out to Lean/Lake and gets exit code 0; sign-off without a genuine rejection is a replay, not evidence. A loose version of this would let a green screenshot or a confident model stand in for a check. This component refuses that. A row counts as accepted only when the runner shells out to Lean/Lake over a temporary copy of the public project and receives exit code 0. A result that can show only sign-off, with no genuine rejection, is treated as a replay, not as evidence.

How it works

Two entry points into _build_result

run drives _build_result with the first-wave fixture and negative cases on; run_certificate_bundle drives it with the exported bundle and negatives off. run calls _build_result with input_mode="first_wave_fixture" and the negative cases on. run_certificate_bundle calls it with input_mode="exported_certificate_kernel_execution_lab_bundle" and the negative cases off, for the standalone public example. The stages below run in _build_result order.

Fixing the source and record boundary

First it enumerates and secret-scans the public inputs, verifies copied source bodies by class, anchors, and SHA-256, and projects them into a citable body floor. First it fixes the source and record boundary. _input_paths enumerates the public Lean files and JSON inputs. scan_paths checks them against core/private_state_forbidden_classes.json. _source_module_manifest_result verifies the exported bundle's copied source bodies by material class, target presence, required provenance anchors, and SHA-256 equality, and returns a finding for any row that fails one of those. _source_open_body_import_summary turns that into a body floor the record can cite by ref, hash, class, count, and verdict, with body_in_receipt: false.

Gathering execution evidence from lake build

Then it copies the project to a temp dir, runs lake build, and sets certificate rows through Lean: accepted rows must return 0, bad rows must fail in their predicted class. Then it gathers execution evidence. For the fixture path it copies the project into a temporary directory, records the public Lean imports, declarations, line counts, and hashes, and runs lake build MicrocosmCertificateLab. If the build returns 0 it sets the certificate transition rows through Lean. Accepted rows must return 0. Missing or bad certificate rows must fail in the residual class the fixture predicted. Typed-repair and bounded-policy rows must rerun inside their allowed action and artifact classes rather than editing arbitrary source.

An obligation graph of public ids only

Then it builds an obligation dependency graph citing public ids only, validated against observed transitions and rejecting any row carrying a proof body, model-output data, oracle template, or private obligation body. Then it builds a dependency graph that is weaker than a proof body and stronger than prose. Each obligation row cites public ids only: an obligation id, dependency ids, transition ids, certificate refs, an evidence kind, and an expected verifier class. The runner validates the rows as a graph over the transitions it actually observed and rejects any row that tries to carry a proof body, a model-output data, an oracle template, or a private obligation body.

The pass floor in _build_result

_build_result returns pass only when the secret scan is clean, Lean and Lake are present, the build returned 0, and the transition, repair, and policy counts each clear their floor; otherwise blocked. _build_result then computes status. It returns pass only when the secret scan has zero blocking hits, Lean and Lake are both available, the build returned 0, at least eight declarations were analyzed, no expected negative case is missing, and the transition, repair, and policy counts each clear their floor. The pass floor requires at least five transitions, three accepted, two residual, one typed-repair effect, and one accepted policy rerun. For the bundle path it also requires the source-body check to pass. Anything short of that is blocked.

flowchart TD inputs["public Lean files and JSON inputs"] scan["scan_paths secret gate"] sources["_source_module_manifest_result copied body check"] build["lake build MicrocosmCertificateLab"] transitions["set certificate rows through Lean"] dag["obligation graph over observed rows"] status["_build_result status pass or blocked"] record["metadata-only result record"] inputs --> scan scan --> sources sources --> build build --> transitions transitions --> dag dag --> status status --> record

Negative cases

Five rejections the fixture must observe

EXPECTED_NEGATIVE_CASES names five rows that must each be rejected with their own error code, and a fixture run missing any of them is blocked because green-only is not evidence. EXPECTED_NEGATIVE_CASES names five rows that must be rejected, each with its own error code. A row that makes provider or oracle text visible to the verifier fails with CERTIFICATE_KERNEL_EXECUTION_PROVIDER_OR_ORACLE_VISIBLE. A typed-repair row carrying a proof body fails with CERTIFICATE_KERNEL_EXECUTION_CP2_PROOF_BODY_FORBIDDEN. A policy row that tries to change source files fails with CERTIFICATE_KERNEL_EXECUTION_EVOLVE_SCOPE_FORBIDDEN. A manifest row pointing at a non-public source refs fails with CERTIFICATE_KERNEL_EXECUTION_PRIVATE_SOURCE_REF_FORBIDDEN. An obligation row carrying a body fails with CERTIFICATE_KERNEL_EXECUTION_OBLIGATION_BODY_FORBIDDEN. A fixture run that does not observe all five is blocked, because a component that can only show green is not evidence that the rejection path is real.

Prior Art Grounding

Proof-carrying code and small-kernel Lean lineage

The design follows the proof-carrying-code and proof-assistant traditions: an untrusted producer supplies a certificate a small trusted Lean kernel checks, with reproducible environments and a named evaluation-scope limit. This component sits in the proof-carrying and proof-assistant traditions. Necula's Proof-Carrying Code anchors the idea that an untrusted producer can supply a certificate checked by a small trusted verifier. The Lean theorem prover continues the small-kernel lineage, and LeanDojo shows why reproducible Lean environments and programmatic proof-state access matter for theorem-proving agents. PBLean is the nearest public reference for the reflective-checker research fork, where a verified Boolean checker imports certificates into Lean without building every explicit proof term. The Lean proof validation reference is the local reason that any move to native or compiler-backed evaluation must be named in the scope limit, not smuggled into an ordinary result record.

Validation Result record Path

Run the first-wave fixture into disposable records from the Microcosm root:

Run the exported bundle through the same component:

cd microcosm-substrate
PYTHONPATH=src ../repo-python -m microcosm_core.organs.certificate_kernel_execution_lab run-certificate-bundle --input examples/certificate_kernel_execution_lab/exported_certificate_kernel_execution_lab_bundle --out /tmp/microcosm_certificate_kernel_execution_lab_bundle

cd microcosm-substrate
../repo-pytest tests/test_certificate_kernel_execution_lab.py -q
cd ..
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a pass means here

A pass certifies only that the project compiled, accepted rows returned 0, each negative case failed in its predicted class, and no proof or provider body reached the record. A pass means the public Lean project compiled, the accepted rows returned 0, every expected negative case was rejected in its predicted class, and the result record carried no proof, provider, oracle, or private-source body.