Verifier Lab Kernel

It is the composition root that runs nine formal-math components and folds their outputs into one public record labelling every row by origin. verifier_lab_kernel is the composition root for the formal-math verifier lab. It runs or consumes nine smaller formal-math components, then folds their outputs into one public result record that labels every row by where it came from.

Not a prover or benchmark runner, it reads a public packet, drives the stack, and sorts evidence into claim buckets, emitting references and verdicts without bodies. It is not a theorem prover, a benchmark runner, a private Lean import, or a frontend surface. It reads a public problem packet, drives the component stack, sorts each piece of evidence into a fixed set of claim buckets, and writes result records that carry references, hashes, counts, and verdicts. The proof text, provider output, oracle answers, and command stdout stay out of what it emits.

The point is separation: one record shows which claims a Lean checker backed, which are provider hints, which are oracle comparisons, and which were rejected. The point is separation. One record shows which claims a Lean checker actually backed, which are provider hints, which are oracle comparisons, and which rows were thrown out for breaking the rules, instead of a pile of separate outputs taken on faith.

Purpose

How progress blurs in a proof loop

In a proof loop a checker sign-off, an oracle match, a provider tactic, and a retrieval hit all look like progress, quietly inflating the count of theorems proved. In a formal-math agent loop several different things look like progress. A Lean checker can accept a term. An oracle holding a hindsight answer can say a candidate matches. A provider model can offer a plausible next tactic. A retrieval step can return a premise. Treated loosely, all of these blur into a single sense of "it worked", and oracle or provider success quietly inflates the count of theorems actually proved.

One authority-class question per row

It stops that blur by asking one question per evidence row, which authority class it belongs to, so a passing component cannot lend its standing elsewhere. This component exists to stop that blur. It answers one question for each row of evidence: which authority class does it belong to, and what may that class claim? A passing component cannot lend its standing to a different bucket.

How it works

Two entry points and the CLI

run drives the fixture with five negative cases, run_kernel_bundle consumes an exported bundle as a synthetic contract, and main is the CLI over both. Two entry points run the kernel. run drives the first-wave fixture with the five negative cases included. run_kernel_bundle drives an exported bundle, where the component result records are consumed as a declared synthetic contract rather than a live run. main is the CLI over both, taking run or run-kernel-bundle with --input and --out.

Both entry points delegate to _build_result, which runs the stages in order: Both entry points delegate to _build_result, which runs the stages in order:

• _load_payloads reads the public packet, the optional proof-lab route file, and any negative-case inputs from the input directory.
• scan_paths, seeded by load_forbidden_classes, scans every input and copied source file for forbidden classes. A blocking hit fails the run.
• _run_component_stack runs each of the nine components on its own fixture (or _standalone_exported_component_stack consumes bundle result records). It normalizes each component record to strip legacy redaction fields and public path roots. The stack passes only when every component status passes.
• _validate_proof_lab_route checks that the declared route resolves to formal_prover_context_strategy_gate and maps to the expected component set.
• _validate_packet runs the five typed row validators (below) over forward problems, oracle structured source record, provider hypotheses, CP2 candidates, and Evolve candidates. Each violation becomes a finding with an error code.
• _claim_separation sorts the validated rows into the seven buckets.

The nine components in the stack

The stack runs nine formal-math components spanning corpus readiness, premise retrieval, tactic routing, trace repair, diagnostics, and the Lean proof witness. The nine components are corpus_readiness_mathlib_absence_gate, lean_std_premise_index, formal_math_premise_retrieval, tactic_portfolio_availability_probe, target_shape_tactic_routing_gate, ring2_premise_retrieval_precision_recall_harness, formal_math_verifier_trace_repair_loop, proof_diagnostic_evidence_spine, and formal_math_lean_proof_witness.

_claim_separation sorts into seven buckets

_claim_separation sorts validated rows into exactly seven buckets, with lean_verified carrying the proof-witness count and contract_rejected holding the observed negative cases. _claim_separation produces exactly seven buckets: lean_verified, provider_suggested, oracle_compared, contract_rejected, retrieval_miss, cp2_translated, and evolve_candidate. The lean_verified bucket carries the proof-witness component status and its compiled declaration count. The contract_rejected bucket carries the observed negative cases, marked as contract violations, not results.

Counters, not description, enforce the boundary

The boundary is enforced by counters that read zero on a clean run, and the status passes only when the scan, component stack, packet validation, and proof-lab route all pass. The boundary is enforced by counters, not description. _build_result computes oracle_forward_success_increment_count (oracle rows that marked themselves as forward success), provider_results_counted (provider rows claiming proof authority), and proof_body_export_count (forward or CP2 rows carrying a proof body). On a clean run these read zero. The final status is a pass only when the secret scan has zero blocking hits, the component stack passes, packet validation passes, and the proof-lab route passes.

_write_receipts emits metadata-only records

_write_receipts emits the public records with body_in_receipt false, the fixture path marking a real runtime result record and the bundle path marking itself a synthetic contract. _write_receipts then emits the public records. The fixture path writes a result record, a board, a validation record, and a fixture sign-off record; the bundle path writes one bundle validation result. Every record sets body_in_receipt to false and carries receipt_transparency_contract, whose omitted_payload_scope is proof, provider, oracle, private-source, and stdout/stderr bodies only. The fixture path marks real_runtime_receipt true on a pass; the bundle path marks itself a synthetic contract and not a live run.

flowchart TD packet["Public packet plus 5 negative cases"] build["_build_result load / scan / validate"] stack["_run_component_stack 9 formal-math components"] buckets["_claim_separation 7 claim buckets"] counters["Authority counters oracle / provider / proof-body = 0"] result records["_write_receipts metadata-only result records"] packet --> build build --> stack stack --> buckets build --> counters buckets --> result records counters --> result records

Negative cases

The fixture carries five named inputs the kernel must reject, each handled by one typed row validator: The fixture carries five named inputs the kernel must reject, each handled by one typed row validator:

• forward_problem_leaks_candidate_body: a forward problem carrying a candidate, ideal, repair, oracle-premise, source-proof, or base-index field. _validate_forward_problems records VERIFIER_LAB_FORWARD_FIELD_FORBIDDEN.
• oracle_counted_as_forward: an oracle structured source record with counted_as_forward_success set true. _validate_oracle_sidecars records VERIFIER_LAB_ORACLE_FORWARD_CONTAMINATION.
• provider_claims_proof: a provider hypothesis asserting proof authority. _validate_provider_hypotheses records VERIFIER_LAB_PROVIDER_PROOF_AUTHORITY_FORBIDDEN.
• cp2_candidate_contains_proof_body: a CP2 row carrying a proof body, raw tactic script, provider body, or oracle template. _validate_cp2_candidates records VERIFIER_LAB_CP2_PROOF_BODY_FORBIDDEN, and it also rejects action classes outside the bounded vocabulary and candidates with no disconfirmation test.
• evolve_mutates_unbounded_artifact: an Evolve row touching an artifact outside the bounded policy set, or asking for arbitrary code mutation. _validate_evolve_candidates records VERIFIER_LAB_EVOLVE_SCOPE_FORBIDDEN, and it also flags candidates that cite no baseline result record.

Each rejected row lands in contract_rejected as a contract violation, never in a claim bucket. Each rejected row lands in contract_rejected as a contract violation, never in a claim bucket.

Prior Art Grounding

LCF composition and LeanDojo boundaries

It follows LCF-style kernel composition that keeps checked results apart from automation, and LeanDojo's lesson that retrieval and provider hints need explicit boundaries. This component follows small-kernel theorem-proving and proof-certificate composition. The LCF approach and HOL Light anchor the idea that a verifier lab keeps trusted checked results apart from heuristics and automation. Lean-oriented work such as LeanDojo adds the agent context: retrieval, provider hypotheses, and proof-state interaction need explicit boundaries before they can influence a proof claim. The kernel borrows the composition discipline and keeps verifier, oracle, provider, CP2, and Evolve rows in separate buckets with separate authority.

Validation Result record Path

Reader validation without durable writes

./repo-pytest tests/test_verifier_lab_kernel.py -q --basetemp=/tmp/microcosm_verifier_lab_kernel_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a pass means here

A pass means the stack runs, the five negative cases are observed, seven buckets hold, counters stay at zero, and no record leaks a body or local root. A pass means the component stack runs, the five negative cases are observed, claim_separation holds exactly the seven buckets, the authority counters stay at zero, and no public record carries a body or a leaked local root.