Formal Math Verifier Trace Repair Loop

Replays how a proof lab turns verifier failures into fixes, with no promotion without a fresh re-run.

Contract

Does It replays how a proof-lab turns a verifier's failure feedback into a teaching signal, working from copied (non-secret) run data so the failure categories, the repair action tied to each failure, and the rule that nothing gets promoted without a fresh re-run result record are all inspectable. Actual proofs, answer keys, and model outputs are deliberately kept out, so the whole correction loop is visible without exposing any of them.

Scope limit It demonstrates control-loop projection mechanics over copied Ring2 run rows only; it does not run Lean/Lake, use external model services, expose proof bodies or oracle premise ids, treat human or provider advice as correctness, prove any theorem, or include launch operations.

Run

Command

microcosm formal-math-verifier-trace-repair-loop run-loop-bundle --input examples/formal_math_verifier_trace_repair_loop/exported_verifier_trace_repair_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_verifier_trace_repair_loop

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Formal Evidence Cell Anchor Resolver, Proof Diagnostic Evidence Spine, Verifier Lab Kernel, Target Shape Tactic Routing Gate, Verifier Lab Execution Spine

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Formal Math Verifier Trace Repair Loop

The public verifier-trace repair fixture validates copied Ring2 failure taxonomy, graph-update, oracle-repair contrast rows, source-module digests, negative cases, and one deterministic toy rerun without claiming proof authority.

Read the full write-up

Back to Components index → Reference roster →