Formal Math Verifier Trace Repair Loop

Verifier failures as repair signals

This is a source-available replay of one proof-lab pattern where a verifier's failure becomes a repair signal, with failure categories, per-failure repair actions, and a no-promotion-without-re-run rule all inspectable from copied data. formal_math_verifier_trace_repair_loop is a source-available replay of one pattern from a proof lab: a verifier reports why an attempt failed, and that failure is turned into a repair signal instead of being thrown away. The component works from copied, run data, so the failure categories, the repair action tied to each failure, and the rule that nothing is promoted without a fresh re-run are all inspectable.

It is not a theorem prover or Lean runner: it validates copied Ring2 rows against their source digests, replays the verifier attempts and repair curriculum, and runs one small deterministic re-run over public inputs. It is not a theorem prover, a Lean or Lake runner, a provider client, or a private import. It validates a bundle of copied Ring2 benchmark rows, checks that the copies match their source digests, replays the verifier attempts and the repair curriculum against those source bodies, and runs one small deterministic re-run over public inputs. The output is a set of metadata-only result records.

Proof and model-output bodies stay excluded

Proofs, oracle answer keys, and model outputs are kept out on purpose, so a row can name a failure class without exposing the proof or oracle premise that produced it. Proofs, oracle answer keys, and model outputs are kept out on purpose. A row can name a failure class without exposing the proof or the oracle premise that produced it.

Purpose

Bookkeeping is where overclaim enters

A failed attempt is cheap to discard and expensive to learn from, and the narrow question is whether its failure can become a reusable public repair signal without inheriting a real prover's authority. A failed proof attempt is cheap to discard and expensive to learn from. The narrow question here is whether a verifier's failure can become a reusable repair signal on the public side, without that signal quietly inheriting the authority of a real prover. The interesting work in a repair loop is the bookkeeping, and bookkeeping is where overclaim usually enters.

A teaching signal needs five fields

A verifier failure counts as a teaching signal only once it carries a trace-backed grade, a repair action named by failure class, a ledger entry, a curriculum edge, and a cold re-run reference. A loose version would collapse the stages into a single verdict: the attempt failed, we fixed it, done. This component refuses that. A verifier failure counts as a teaching signal only once it carries a trace grade backed by trace events, a repair action named against the verifier failure class it answers, an entry in the failure-mode ledger, a curriculum edge, and a cold re-run reference. Each of those is a separate field, and promotion is blocked until the cold re-run reference is present.

Guarding against stale copied rows

The guarded failure is stale copied rows pretending to be live proof-lab evidence, so the copies are re-checked against their sources on every run and the verdict is downgraded on any drift. The failure mode it guards against is stale copied rows pretending to be live proof-lab evidence. The rows are imported from one real Ring2 benchmark run, so the temptation is to treat the copy as if the run were happening now. The answer is to re-check the copies against their sources on every run and downgrade the verdict when anything drifts.

How it works

Two entrypoints, one builder

run validates a fixture with the eight negative cases and run_loop_bundle validates an exported bundle under the stricter source-module path, both calling _build_result, which passes only with every check green and no negative case missing. There are two entrypoints. run validates a fixture directory with the eight negative-case files included. run_loop_bundle validates an exported bundle: it computes a freshness digest over the inputs, can reuse a current result record, and runs the stricter source-module path that requires every copied body to match its manifest. Both call _build_result, which composes the checks below in order and returns one record. A run is a pass only when every check passes and no negative case is missing.

validate_projection_protocol demands provenance

validate_projection_protocol requires each copied row to keep its source_ref, source_sha256, target and validation refs, and copied-material status, blocking thin or unprovenanced projections. validate_projection_protocol reads the projection manifest. It requires copied-material provenance: each copied row must keep its source_ref, source_sha256, target refs, validation refs, and a copied-material status, and any omitted proof, oracle, or provider material must carry an omission reference. Thin or unprovenanced projections are blocked.

validate_source_module_manifest is the strict gate

validate_source_module_manifest requires a import class, body_in_receipt: false, and a matching digest, line, and byte count per Ring2 source ref, emitting typed mismatch findings on any drift. validate_source_module_manifest is the strict gate, required for the exported bundle. It requires a import class, body_in_receipt: false, one row per declared Ring2 source ref, and for each row a matching digest, line count, and byte count against the copied file on disk. Drift produces typed findings such as VERIFIER_TRACE_SOURCE_MODULE_DIGEST_MISMATCH, VERIFIER_TRACE_SOURCE_MODULE_SIZE_MISMATCH, or VERIFIER_TRACE_SOURCE_MODULE_COUNT_MISMATCH. The exported bundle carries seven source modules and all seven must verify.

validate_verifier_attempts replays each attempt

validate_verifier_attempts checks each attempt's verifier class and trace events, then _validate_attempt_source_replay dereferences the premise, oracle-contrast, and candidate rows, counting attempts, events, actions, and promotions. validate_verifier_attempts checks each attempt for a verifier class and trace-event metadata, then hands the row to _validate_attempt_source_replay, which dereferences the premise-run row, the oracle-repair contrast row, and the graph-update candidate named by the attempt. Mismatches become VERIFIER_TRACE_SOURCE_REPLAY_MISMATCH, VERIFIER_TRACE_ORACLE_REPLAY_MISMATCH, VERIFIER_TRACE_COLD_RERUN_SOURCE_MISMATCH, or VERIFIER_TRACE_CANDIDATE_REPLAY_MISMATCH. It counts attempts, trace events, repair actions, and cold-rerun promotions.

Curriculum and promotion policy checks

validate_repair_curriculum rejects a ledger append accepted after a cold re-run with no reference, and validate_promotion_policy requires cold_rerun_receipt_ref and rejects a policy setting formal_proof_authority true. validate_repair_curriculum checks the failure-mode ledger and the curriculum edges, and rejects a ledger append marked accepted after a cold re-run that has no cold re-run reference. validate_promotion_policy requires cold_rerun_receipt_ref in the policy's promotion requirements and rejects a policy that sets formal_proof_authority to true.

The one thing actually executed

_run_toy_theorem_repair_rerun is the only executed step: over inputs 0, 1, 2, 7 the failing candidate returns constant 0 and the repair returns n, plain integer arithmetic, not a Lean proof. _run_toy_theorem_repair_rerun is the one thing actually executed. It takes the toy statement toy_add_zero_identity over the inputs 0, 1, 2, and 7. The failing candidate sets the right side to the constant 0, which fails on three of the four inputs. The repair sets the right side to n, which passes on all four. It is plain integer arithmetic over public inputs through _eval_toy_expr, not a Lean proof.

Grading the run from R1 to R4

_runtime_realness_evidence reaches R4 only for a fully verified bundle with 30-plus clean source-replay checks and a passing toy re-run, dropping to R3 on any mismatch, R2 for fixtures, and R1 otherwise. _runtime_realness_evidence grades the run. It reaches R4 only for an exported bundle with all seven source modules verified, at least 30 source-replay checks with zero mismatches, at least three attempts, at least nine trace events, at least three failure modes, and a passing toy re-run. A verified bundle with any source-replay mismatch drops to R3 (mutated trace rejected). A fixture with copied material and observed negative cases sits at R2. Everything else is R1, the metadata floor. _write_receipts then emits the result record, a board, a validation record, and a fixture-pass record, all metadata-only.

flowchart TD Input["Fixture or exported bundle copied Ring2 rows + source manifest"] Protocol["validate_projection_protocol copied-material provenance"] Manifest["validate_source_module_manifest digest, line, byte match; body_in_receipt false"] Attempts["validate_verifier_attempts trace events, verifier class, source replay"] Curriculum["validate_repair_curriculum failure-mode ledger, curriculum edges"] Promotion["validate_promotion_policy requires cold re-run ref"] Toy["_run_toy_theorem_repair_rerun fail on 0, repair to n"] Realness["_runtime_realness_evidence clean replay to R4; any drift downgrades"] Result records["_write_receipts result, board, validation, fixture-pass"] Input --> Protocol Protocol --> Manifest Manifest --> Attempts Attempts --> Curriculum Curriculum --> Promotion Promotion --> Toy Toy --> Realness Realness --> Result records

What the shipped bundle produces

On the shipped exported bundle this produces five attempts, 15 trace events, five repair actions, three cold-rerun promotions, seven verified source modules, 37 clean source-replay checks, and an R4 grade. On the shipped exported bundle this produces five attempts, 15 trace events, five repair actions, three cold-rerun promotions, three failure modes, three curriculum edges, seven verified source modules, 37 source-replay checks with zero mismatches, and an R4 grade.

Negative cases

The fixture path carries eight named negative files, and EXPECTED_NEGATIVE_CASES requires each to be observed before a pass. The fixture path carries eight named negative files, and EXPECTED_NEGATIVE_CASES requires each to be observed before a pass. Each maps to one error code:

• attempt_with_proof_body produces VERIFIER_TRACE_PROOF_BODY_FORBIDDEN.
• attempt_with_oracle_ids produces VERIFIER_TRACE_ORACLE_IDS_FORBIDDEN.
• trace_grade_without_trace produces VERIFIER_TRACE_GRADE_WITHOUT_TRACE.
• repair_without_verifier_class produces VERIFIER_REPAIR_WITHOUT_VERIFIER_CLASS.
• promotion_without_cold_rerun produces VERIFIER_PROMOTION_WITHOUT_COLD_RERUN.
• provider_payload_leakage produces VERIFIER_PROVIDER_PAYLOAD_FORBIDDEN.
• human_approval_as_proof produces VERIFIER_HUMAN_APPROVAL_NOT_PROOF_AUTHORITY.
• repair_claims_theorem_correctness produces VERIFIER_REPAIR_CLAIMS_THEOREM_CORRECTNESS.

Why repair metadata is not a truth claim

A repair trace that sets a theorem-correctness flag is rejected, so the loop can say what to try next without saying the theorem is true, and mutations downgrade the grade rather than passing quietly. The last case is why repair metadata cannot become a truth claim: a repair trace that sets a theorem-correctness flag is rejected, so the loop can say what to try next without saying the theorem is true. The focused tests also perturb an oracle source row, a manifest digest, an attempt source label, and a curriculum source count, and confirm each mutation downgrades the grade rather than passing quietly.

Prior Art Grounding

Proof-attempt feedback loops

The component follows interactive theorem-proving feedback loops like GamePad, HOList, and LeanDojo, borrowing the accounting shape of separate verifier-event, grade, failure-class, repair, and cold-rerun fields without treating advice as correctness. This component follows interactive theorem-proving feedback loops where failed proof attempts become structured training or repair signals. GamePad and HOList expose theorem-proving interaction data for machine-learning experiments, and LeanDojo keeps proof-assistant feedback, retrieval, and proof-state interaction reproducible. What is borrowed is the accounting shape: verifier events, grades, failure classes, repair actions, curriculum deltas, and cold re-run references stay separate fields. Human or provider advice is not treated as formal-result correctness.

Validation Result record Path

Run these from the repo root without mutating durable result record surfaces:

./repo-pytest tests/test_formal_math_verifier_trace_repair_loop.py -q --basetemp=/tmp/microcosm_formal_math_verifier_trace_repair_loop_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.relationships.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/formal_math_verifier_trace_repair_loop.json

What a pass means here

A pass means the fixture and bundle replay hold, the eight negative cases are observed, the copied bodies match their digests, and the row reports edge_count: 17, but no theorem is proved. A pass means the fixture and exported-bundle replay hold, the eight negative cases are observed, the copied bodies match their digests, and the generated row reports edge_count: 17, source_authority: json_capsule, and zero unresolved selective relations. It does not mean any theorem is proved.