Strict Lean 4 verifier (Track L / P1)
A reward and an evaluator for formal proofs that cannot be gamed by "it compiles". Code:
align/verify/lean/ (stdlib only), installer scripts/lean_setup.sh, ceiling test
scripts/lean_ceiling_test.py (+ frozen case tables scripts/lean_ceiling_cases.py), tests
tests/test_lean_verifier.py. The Lean toolchain is an external binary
(docs/DEPENDENCY_POLICY.md, "External binary: Lean 4 toolchain"), reached only through
subprocess.
Status (2026-10-12): implemented, tested without Lean (173 tests, fake REPL), tested against the real toolchain (19 slow tests), mutation-tested (40 hand mutants), and ceiling-tested:
| Known-good accepted | 177 / 178 = 99.44 % (Wilson 95 % [96.9 %, 99.9 %]); floor 98 % -> PASS |
| Adversarial accepted | 0 / 61 -> PASS (a compile-only grader would have paid 51) |
| Throughput, 8 workers | 0.57 proofs/s on a heavy unfiltered mix; 4.4 proofs/s on the median mix (GRPO shape) |
| Memory per warm REPL | 0.64-0.65 GiB PSS with 8 workers (0.24 GiB private); 0.85 GiB peak under load |
| Install | 5.57 GiB, 3 min; import Mathlib 3.2 s warm / 39.7 s cold |
Section 5 holds the numbers; every figure there is copied from a file under .tmp/lean_ceiling/.
Section 4 is the pre-registration. Section 6 lists what this verifier does not promise.
1. The pin
| Lean | leanprover/lean4:v4.9.0-rc1 (lean --version: 4.9.0-rc1, commit be6c4894e0a6) |
| Mathlib | leanprover-community/mathlib4@d1d1e4b72c6e009edd97cabe1d661b021fe8eeae (2024-06-12) |
| REPL | leanprover-community/repl@v4.9.0-rc1 (7df77c0a1c91), built against the same toolchain |
| elan | 4.2.4 |
| Location | /apps/development/rlhf/lean/ (elan/, workspace/ = Lake project requiring Mathlib at the rev above, repl/, PINS.json) |
Provenance (how "the Goedel-Prover-V2 pin" was determined, not assumed). Goedel-Prover-V2's
README says "we follow DeepSeek-Prover-V1.5, which uses Lean 4 version 4.9 and the corresponding
Mathlib". The repo's mathlib4 git submodule is xinhjBrant/mathlib4 at commit
2f65ba7f1a9144b20c8e7358513548e317d26de1. That commit is a single child (message align,
2024-08-07, Huajian Xin of DeepSeek) of upstream d1d1e4b72c6e, and changes only
lakefile.lean and lake-manifest.json to add xinhjBrant/repl@deepseek as a Lake dependency;
its lean-toolchain is leanprover/lean4:v4.9.0-rc1. So "Lean 4.9" in that README is
nominal: the binary is 4.9.0-rc1, not 4.9.0.
Deviation, and why it is safe. We pin the upstream parent and build the REPL separately.
Mathlib's prebuilt .olean cache is keyed on a hash that includes lakefile.lean, so the
DeepSeek child commit would not hit the cache and would force a multi-hour Mathlib build. The
parent's Mathlib sources, and therefore the .oleans, are byte-identical to what the child
compiles; the only difference is which REPL fork the lakefile names. We use upstream
repl@v4.9.0-rc1, whose protocol (cmd/env) is all this package needs. The fork's extra
options (allTactics, ast, premises) are not used. Install cost with the cache: 3 minutes,
5.8 GB (Section 5).
Version drift is a correctness issue. SafeVerify keeps separate branches for 4.9.0 and 4.15.0; PutnamBench moved to 4.33.1 in 2026-09. Proofs verified here say nothing about 4.33. Every number this verifier produces must be reported with this pin and the verifier tier.
2. Architecture and what each layer defends
completion text ──extract_lean_code──▶ code ──static_check──▶ Plan
(reward.py) (strict.py: lexer, bans, header, target)
│ reject: no Lean touched
▼
ReplPool.acquire ─▶ Worker: [import once] ─▶ [audit prelude] ─▶ [header opens]
(repl_pool.py) │
ref = `theorem _align_ref <given signature> := sorry` ──▶ env R
candidate body, run in env R ──▶ env C (errors / sorry ⇒ reject)
`#align_audit "<nonce>" 1 <target> _align_ref` in env C ──▶ verdict JSON
| Layer | Rejects | Independent of the lexer? |
|---|---|---|
extract_lean_code |
no fence / truncated (unclosed) fence / prose | n/a |
| header equality | any change to imports, opens, options (token-for-token vs the reference header) |
yes (token compare) |
| lexical bans | sorry/admit, native_decide, unsafe/partial, implemented_by/extern/export, axiom/opaque, macro/elab/syntax/notation/run_cmd/initialize, any #cmd, namespace/section/variable/attribute/local, instance, def/abbrev (unless allow_helper_defs), Lean.*/IO.* identifiers, exact?/apply?, non-whitelisted set_option (incl. maxRecDepth > 16384), attributes that change compilation/elaboration |
no (this is the lexer) |
| target rules | target missing, declared twice, private/protected/attribute on it, signature tokens differ from the reference's (strict mode) |
no |
| compile | any error; any sorry warning; non-empty sorries |
yes (Lean) |
| audit: axioms | any axiom outside {propext, Quot.sound, Classical.choice}: catches sorryAx, Lean.ofReduceBool/trustCompiler (native_decide), user axioms, even if the lexer were fooled |
yes |
| audit: statement bridge | the kernel is asked to check theorem _align_bridge : <type of _align_ref> := <candidate>. _align_ref was elaborated before the candidate existed, so a definition-hole (instance, variable, shadowing) that makes the same text mean something else fails here |
yes |
| audit: kernel recheck | every local theorem re-added with debug.skipKernelTC forced off |
yes |
| audit: meta-declaration scan | a NEW local constant whose type/value mentions Lean.Elab/Meta/Macro/Parser/PrettyPrinter/Syntax/Environment/Core/Compiler, IO, unsafeCast: the footprint of an elab/macro that slipped past the lexer |
yes |
| audit: kind | the target must be a theorem (not a def that happens to inhabit the type) |
yes |
The audit verdict is the one info message tagged ALIGN_AUDIT <random nonce>, produced by a
separate REPL call after the candidate ran. The candidate's own output cannot carry the
nonce (it is generated after the candidate text is fixed), so it cannot forge a verdict.
Reward semantics (reward.py): accuracy ∈ {0,1}, 1 only if every layer passes. Diagnostics
(StrictResult.reasons, .diagnostics) are returned separately and never folded into the
reward: shaped partial credit ("compiles but has sorry") is exactly the gradient a policy
follows to the exploit (Leanabell-V2 also found shaped rewards slightly worse than binary).
Plug-in points, none of which change the loss or CompositeReward:
from align.verify.lean import ReplPool, StrictVerifier, LeanAccuracy, find_toolchain
pool = ReplPool.from_toolchain(find_toolchain(), preflight=True) # host rules + worker count
acc = LeanAccuracy(StrictVerifier(pool))
accuracy, result = acc.score(formal_statement, completion_text) # float in {0,1}, diagnostics
terms, result = acc.reward_terms(composite, formal_statement, completion_text, fmt, n_tokens)
outcomes = acc.verify_batch(statements, completions) # OutcomeVerifier surface
Failure semantics. A proof that times out, exhausts memory or kills its REPL scores 0 (that
is a property of the proof). A dead verifier must not: LeanInfraError is raised when the
base environment cannot be built or when more than half of a batch (of at least 8) died for
infrastructure reasons. Otherwise a broken toolchain would feed the policy an all-zero reward
that reads as "the model got worse" (the 0/100 perfect-policy incident, mirrored).
Failure taxonomy (StrictResult.reasons): no_code, parse_error, unsupported_statement,
header_mismatch, target_missing, target_modifier, statement_mismatch, banned:<x>,
compile_error, sorry, not_theorem, axiom:<name>, bridge_failed (defeq mode),
kernel_recheck_failed, meta_decl, skip_kernel_tc, timeout, crash, memory,
output_too_large, protocol, reference_invalid.
Statement modes. strict (default): signature tokens equal the reference's and the kernel
bridge passes. defeq: bridge only, so an alpha-renamed or restated-but-defeq signature is
accepted. The bridge is checked by the kernel (not the elaborator's isDefEq), so "accepted"
means "the candidate's constant has a type the kernel accepts as the reference's type".
3. REPL pool: measured facts the design rests on
| Fact (measured on this box, Lean 4.9.0-rc1 + Mathlib pin) | Consequence in code |
|---|---|
| The REPL does not flush stdout when it is a pipe (only a pty line-buffers); the client blocks forever | binary wrapped in stdbuf -o0 -e0 (tests::test_wrapped_argv_*) |
lake env prints cwd-relative paths (././.lake/...) |
absolutised once in toolchain.build_child_env; child gets a minimal environment (no tokens) |
A second fresh import Mathlib in a live process cannot re-mmap the .oleans and reads them into the heap: Pss_Anon 0.25 → 4.14 GiB |
one import per process; every header variant is layered on it (split_imports, Worker.header_env); a different import set recycles the process |
RSS is ~3.65 GiB but 3.40 GiB of it is the shared, read-only .olean mapping; private heap is ~0.25 GiB |
the watchdog caps Pss_Anon, not RSS; plan_workers budgets shared-once + n × cap |
Nat.pow exponent is too big and lean::stack_space_exception abort the process (rc=1, rc=-6) |
ReplCrash with the stderr tail; the next acquire respawns; scored 0 |
debug.skipKernelTC is an unknown option on 4.9.0-rc1 |
the whitelist + the audit's skip_tc check are guards for a pin upgrade, not a live exploit here |
Lean 4.9 has no public collectAxioms (#print axioms is private) |
alignCollectAxioms in the prelude (same traversal) |
variable (h : False) used in a proof body is added to the theorem's type in 4.9 (pre-4.11 behaviour) |
variable is banned lexically and the bridge catches it independently |
Limits per worker (defaults, ReplLimits): anonymous-memory cap 4 GiB (watchdog polls
smaps_rollup every 0.5 s), prlimit --as=16GiB --fsize=256MiB --core=0, nice +5, output cap
16 MiB, per-proof wall budget 180 s (compile + audit), SIGKILL of the whole process group on any
violation, MALLOC_ARENA_MAX=2. Workers recycle after 1000 commands. Default worker count is
min(8, cores // 4) = 8 on this box; ReplPool.from_toolchain(preflight=True) applies the
/apps/CLAUDE.md checks (≥ 45 GB MemAvailable, load < 2× cores, disk queue < 64) through
align.utils.guard.preflight_host_check and then shrinks the worker count so that, even with
every worker at its cap, MemAvailable stays above the 45 GB floor. The ceiling-test script
takes the same exclusive heavy-job flock as the trainers (a Lean pool is a heavy job).
4. Pre-registration (written BEFORE the registered ceiling run)
Registered 2026-10-12 20:12 IST, before any run of scripts/lean_ceiling_test.py without
--allow-unregistered. The case tables (HEADER, STATEMENTS, ADVERSARIAL, RESTATED in
scripts/lean_ceiling_cases.py) are frozen by hash:
PREREG_TABLE_SHA256: 61636c7136eb647801c588b00a35bd8bcc6ef4db126c21ea75769092883ff7e2
python scripts/lean_ceiling_test.py --verify-prereg recomputes it; the registered run refuses
to start on a mismatch.
Honest note on process. The tables were developed against this verifier (about six exploratory
runs on 1-2 workers, --exploratory --allow-unregistered) so that every adversarial case is
live (it would be paid by a compile-only grader, which the run also measures) and every
restated proof compiles. Those exploratory runs informed case authoring only; thresholds
below were fixed before the registered run, and any verifier change after registration that
alters a verdict is reported as an amendment in Section 7, with the pre-amendment matrix kept.
Configuration under test = shipped defaults: StrictConfig() (strict statement mode, no helper
defs, kernel recheck ON, 180 s budget per proof) and ReplLimits() (4 GiB anonymous cap, 16 GiB
--as backstop), 8 workers, lean_workbook compile-only filter budget 120 s.
Known-good set. (a) Public verified proofs: 6 contiguous slices of 25 rows at offsets
0, 5000, 10000, 15000, 20000, 25000 of Goedel-LM/Lean-workbook-proofs (29,750 proofs verified
under the Lean 4.9 / DeepSeek-Prover-V1.5 Mathlib environment), fetched over HTTP, never the
full dataset. (b) 30 hand-restated Mathlib-style theorems with proofs. The formal statement
given to the verifier is derived mechanically from each proof file (header + last theorem's
signature cut at the signature-ending := + sorry). Filter: an independent compile-only
pass (same REPL, no strictness: no error message and no sorry warning) defines "compatible
with the pin"; items failing it are excluded and listed. Scored population = compile-clean
items. Pass: ≥ 98 % accepted and ≥ 50 items. (The roadmap's P1 row says ≥ 99 %; the task
fixed 98 %, which is what is registered. Both are reported.) Any rejected known-good item is
listed with its reasons; rejections caused by the policy bans (e.g. a genuine native_decide
in a public proof) count as failures, because that is the cost the RL stage would pay.
Adversarial set. ≥ 30 hand-built cases, all registered (61): categories sorry (7), admit (2), extra axiom (4), native_decide (3), changed statement (6), weakened hypothesis (3), definition hole (4), environment manipulation via elab/macro/run_cmd/initialize/#eval/#exit (9), theorem proved for a different name (6), timeout/crash/memory bombs (3), banned constructs (6), header tampering (4), no code (4). Each is a completion (prose + fenced block) so fence extraction, static gate, REPL compile and audit are all exercised. Pass: 0 accepted. Bomb cases run on a dedicated 1-worker pool (1 GiB anonymous cap, 30 s budget) so they terminate promptly; the code path is the same. Reported alongside, not part of the pass criterion: how many cases a compile-only grader would pay; and which cases the Lean-side audit rejects on its own with the lexical gate disabled.
Confusion matrix (reported verbatim): rows = truth (good / bad), columns = verdict (accept / reject); good = compile-clean known-good, bad = adversarial.
Measurements (reported, no threshold): install disk size; import Mathlib cold
(page cache evicted with posix_fadvise(DONTNEED)) and warm; per-REPL PSS / Pss_Anon / RSS from
/proc/<pid>/smaps_rollup with Mathlib imported, for one process and for 8 concurrent workers;
throughput (proofs/s) at the worker count used, with the worker set warm, on unique statements
and in the GRPO shape (12 statements × 8 samples); latency p50/p90/p99; PSS sampled during the
run.
5. Results
All numbers below are copied from .tmp/lean_ceiling/registered/result.json and
.tmp/lean_ceiling/registered.log (the registered run: hash verified, prereg_registered=true,
8 workers, host preflight passed, heavy-job lock taken after waiting for another track's job
to release it, started ~20:13 IST, 2026-10-12). Host: 48 cores; MemAvailable never fell below
136.9 GB in the samples taken during the strict known-good pass.
5.1 Ceiling test: confusion matrix (verbatim)
verdict ACCEPT verdict REJECT total
truth GOOD proofs 177 1 178
truth BAD proofs 0 61 61
| Criterion (pre-registered) | Measured | Verdict |
|---|---|---|
| known-good accepted >= 98 %, n >= 50 | 177 / 178 = 99.44 % (Wilson 95 % [96.89 %, 99.90 %]); n = 178 | PASS (also >= the roadmap's 99 %) |
| adversarial accepted = 0, n >= 30 | 0 / 61 | PASS |
| gate 5 of the roadmap: strict false-negative rate > 5 % blocks P2 | 0.56 % (upper Wilson 3.1 %) | not blocked |
Known-good population. 180 candidates (150 Lean-Workbook-proofs rows from dataset revision
b731852af8d8, raw file sha256 55932494...aebef; 30 restated). The independent compile-only
filter kept 178: 148 + 30. The 2 excluded (lean_workbook_10036, lean_workbook_plus_64037)
were excluded because the compile-only pass hit its 120 s budget (why: timeout), not because
of a compile error, so "version-incompatible" would be the wrong label: they are slow proofs.
All 30 restated proofs were accepted.
The one rejected known-good proof: lean_workbook_51088, reason timeout (180 s strict
budget). It is a nlinarith proof with nine hints. Follow-up (exploratory, 1 worker, not part of
the registered numbers), same proof, same pool code, only the REPL environment layers differ:
| environment the body runs in | wall time |
|---|---|
| imports + header (what the compile-only filter uses) | 99.9 s (filter: 104.1 s) |
+ reference theorem _align_ref |
225.8 s |
| + audit prelude | 513.6 s |
| + both (= the strict path) | 516.5 s (timed out at 400 s in a separate strict run) |
On lean_workbook_10009 (20 s) the same four environments take 19.9 / 20.8 / 20.1 / 20.0 s. So
this is not a systematic strict-tier slowdown; it is the well-known run-time chaos of a borderline
nlinarith (the certificate search is sensitive to state it inherits from earlier commands) hitting
a 180 s wall-clock budget. It is a genuine false negative of the reward (such a proof would score
0), it is bounded at one in 178 here, and raising the budget to Goedel's 300 s would not have saved
it (517 s). The honest reading: wall-clock-bounded verification of proofs this close to the limit is
flaky in BOTH directions, so for evaluation (not training) report results at a stated budget.
Adversarial population (61 cases, all rejected). First reason per case: 58 rejected by the
static gate (no Lean call), 3 by the REPL layer (the bombs). By category (cases / accepted):
sorry 7/0, admit 2/0, extra_axiom 4/0, native_decide 3/0, changed_statement 6/0,
weakened_hypothesis 3/0, definition_hole 4/0, env_manipulation 9/0, wrong_name 6/0,
timeout_bomb 3/0 (timeout, rc=-6 stack-overflow crash, anonymous-memory kill at 1110 MiB over a
1024 MiB cap), banned_construct 6/0, header_tamper 4/0, no_code 4/0.
- A compile-only grader would have paid 51 of the 54 code-bearing, non-bomb cases
(each case's own text compiled with no strictness). The 3 it would not:
header_missing(no Mathlib),duplicate_target(Lean itself rejects a duplicate name) andskipKernelTC_option(unknown option on this Lean). The 3 bombs and the 4no_codecases are not applicable. So 51 are live exploits, not strawmen. - Semantic layer alone (lexical gate OFF, so each exploit actually executes inside Lean, with
kernel_recheckon): rejected 45 of the 54 code-bearing non-bomb cases by the Lean-side audit alone (sorry,axiom:bad,axiom:Lean.ofReduceBool,axiom:evilafter anelabadded an axiom,statement_mismatchfor the instance hole, thevariablehole, shadowing viamacro_rules, changed constants/hypotheses,meta_declforinitialize,target_missingfor wrong names/namespaces/private targets,header_mismatch). The 9 it accepted are the policy-only set, where the proof of the stated theorem is valid and the lexical ban is the only thing stopping it:eval_side_effect,exit_after_theorem,attribute_on_target,unsafe_implemented_by,partial_def,extern_attr,search_tactic_exact_q,maxRecDepth_abuse,helper_def_with_proof. None is a soundness gap (the theorem is proved); they are rejected to keep the attack surface small, and each costs real-world proofs that use them (Section 6, item 5).
5.2 Install and process measurements
| Quantity | Measured |
|---|---|
Install time (lean_setup.sh, cache hit) |
3 min 9 s (18:23:06 -> 18:26:15); an idempotent re-run takes ~10 s |
| Disk, total | 5,981,549,078 B = 5.57 GiB: elan + toolchain 0.93 GiB, workspace 4.34 GiB (of which Mathlib package 4.11 GiB), REPL 94 MiB |
import Mathlib + Aesop, cold (page cache for all 11,171 .olean/.ilean/.so files = 4.19 GiB evicted with posix_fadvise(DONTNEED)) |
39.7 s |
| same, warm (3 runs) | 3.19, 3.20, 3.19 s (median 3.19 s) |
| 8 workers warmed in parallel | 3.38 s (warm cache) |
| One REPL after the import (alone on the box) | RSS 3439 MiB, PSS 3437 MiB, Pss_Anon 244 MiB, Pss_File 3193 MiB, 1 thread, VmSize 4071 MiB |
| Per-worker PSS with 8 workers all holding Mathlib | 643-653 MiB each (mean 648; RSS 3.4-3.5 GiB each) = 244 MiB anonymous + 3193 MiB / 8 shared. Sum of PSS 5.06 GiB; sum of RSS 26.8 GiB (the double count the PSS figure removes) |
| Per-worker PSS during the 178-proof run (sampled every 0.5 s) | mean 717-792 MiB, max 873 MiB; Pss_Anon max 404 MiB; RSS max 3.65 GiB |
| Worker growth over 1042 commands | none that approached any limit: recycled 0 times (limit 1000/worker) |
fincore was not usable for confirming the eviction (its output did not parse into a residency
fraction: the script printed None and 4096.0; ignore those two fields in result.json). The 12x
cold/warm gap is the evidence that the eviction worked.
Model implied by the measurements: PSS(n workers) ~ 0.24 GiB + 3.12 GiB / n per worker, total
~ 3.12 + 0.24 n GiB. Eight workers cost ~5 GiB of RAM in total. The worst case (all eight at
their 4 GiB anonymous cap) is 3.12 + 8 x 4 = 35 GiB, which is what plan_workers budgets against
the 45 GB floor, so the pool cannot push MemAvailable under the floor on this host. Roadmap gate 5 ("above ~4 GB per warm REPL the pool
shrinks below ~8 workers") is not triggered: 0.65 GiB per warm REPL, 0.85 GiB peak under load.
5.3 Throughput (8 workers, warm)
| Shape | Proofs | Wall | Proofs/s | Notes |
|---|---|---|---|---|
| 178 unique statements (the known-good set, strict tier incl. kernel recheck) | 178 | 310.9 s | 0.573 | latency p50 1.97 s, p90 21.4 s, p99 158.6 s, max 180.3 s (the timeout), mean 9.76 s |
| GRPO shape: 12 median-latency statements x 8 identical samples | 96 | 21.9 s | 4.38 | reference environment and baseline audit reused per worker; all 96 accepted |
The first number is dominated by the heavy tail of Lean-Workbook nlinarith proofs (mean 11.7 s,
median 2.65 s for those; the 30 restated proofs: median 0.18 s, max 1.5 s) and by one 180 s
straggler: the ideal packing of the work is 178 x 9.76 s / 8 = 217 s. It is not a verifier
overhead: the compile-only filter took 273 s for 180 candidates on the same 8 workers, i.e. the
strict tier added 14 % (audit 0.03-0.7 s per proof; kernel recheck +0.04-0.12 s on 20-43 s
proofs). Against the research report's guess of "1-3 proofs/s for 8-16 workers (low confidence)":
0.57/s on a heavy, unfiltered population and 4.4/s on a median population; either way
verification stays far above generation (0.1-0.17 proofs/s per the report), so it is not the
binding constraint at this worker count.
5.4 Test and mutation evidence
pytest tests/test_lean_verifier.py -m "not slow": 173 passed (no Lean needed; fake REPL binary speaks the real protocol, including the audit message).pytest tests/test_lean_verifier.py -m slow: 19 passed on the real toolchain (accepts a correct proof, rejects eight exploits with the lexical gate OFF, defeq-vs-strict mode, invalid reference, timeout + recovery, end-to-end reward path, concurrency, memory shape).tests/test_dependency_firewall.py: 2 passed (align/verify/lean/and the two scripts import only stdlib /align).
6. Residual risks (what this verifier does NOT promise)
- Lexer desync. The lexical gate is a hand-written tokenizer, not Lean's. It follows Lean's
rules for nested comments, string escapes, raw strings, char literals and
«», and on any unusual construct falls back to a raw-text scan, but it has not been differentially fuzzed against Lean's real tokenizer. Mitigation: layers 3+ (axioms, bridge, kernel recheck, meta-declaration scan) do not use it; the semantic-only column of the ceiling test shows what they catch alone. What only the lexer stops is listed there (all of it is policy, not soundness: the proofs are valid for the stated theorem). - No OS sandbox. The REPL runs as the same user with filesystem access and no
network namespace. Code can only execute inside the elaborator through meta-programming
(
elab/macro/run_cmd/#eval/initialize/unsafe), all of which are banned lexically AND detected by the meta-declaration scan, and the child's environment holds no secrets (toolchain.build_child_env). A meta-programming escape that evades both would run with the verifier's file permissions. For adversarial RL, run the pool as a dedicated unprivileged user or underunshare --net/ a cgroup; that needs privileges this task did not have. - Statement fidelity. The bridge proves the candidate proves the GIVEN formal statement. It says nothing about whether that statement means what the informal problem says (miniF2F: formal/informal discrepancies in over half the problems, 16 unprovable statements; the report, section 5F). Report miniF2F-v2/PutnamBench with the pin and tier.
- Trust base. The Lean kernel,
propext,Quot.sound,Classical.choice, the REPL, and the prelude (AUDIT_PRELUDE, ~100 lines). The prelude is a trusted program; it is exercised by the real-toolchain tests, not formally verified. - Policy rejections are not soundness failures.
def/instance/notation/namespacehelpers,exact?,#evaland so on are rejected even when the proof of the stated theorem is valid. That is deliberate (smaller attack surface) and has a cost: public proofs that use them are false negatives.allow_helper_defs=Truerelaxes onlydef/abbrev. - Version drift. Proofs from other Lean/Mathlib versions will fail to compile (counted as 0), which is correct for this pin and wrong as a statement about the proof.
- Throughput numbers are for this population (short Lean-Workbook-style and restated
proofs). A prover that emits long
nlinarith/decideproofs will be slower; the audit costs ~0.3 s for proofs whose dependency closure reaches real analysis and ~0.03 s foromega.
7. Amendments
7.1 Changes between the exploratory runs and the registration (before 20:12 IST; not
amendments, listed so nothing is hidden). Case-table edits made after seeing exploratory output:
sorry_branch (its all_goals sorry was dead code, so the proof was valid: moved the sorry into
a live branch); sorry_after_char_quote / sorry_after_comment_opener_string (did not compile;
rebuilt so the sorry really sits between two quote-bearing literals); axiom_private,
axiom_reducible_attr (did not compile; replaced by axiom_polymorphic, axiom_via_simpa);
ofReduceBool_term (rfl cannot discharge Lean.reduceBool; replaced by
native_decide_in_helper_lemma); local_notation_hole (a local + notation is ambiguous with
the builtin one, so it never elaborates; replaced by variable_hole_hypothesis);
rs_default_arg (did not compile). Verifier changes made before registration, each driven by a
measurement: single import per process (Section 3), the late-answer drain, kernel_recheck
default, the open Lean-root ban, notation3/binder_predicate/... bans, 180 s default budget,
split_imports/prelude-before-opens layering. The skipKernelTC_option case turned out to be
inert on this pin (the option does not exist) and was kept, labelled.
7.2 Retraction. A first measurement reported the kernel recheck as costing "2.2-3.2x"
(lean_workbook_10009: 21 s -> 68 s). That reading came from a run on a host where two other
Lean processes were competing; isolated measurements (#align_audit flags 0 vs 1 on the same
environment) show +0.04 to +0.12 s against 20-43 s of elaboration. The recheck is therefore ON
by default; the claim was removed from the code comment before registration. (The same episode is
why the headline timings here come from the registered run; the few ad-hoc timings are labelled
exploratory.)
7.3 Verifier changes after registration: none. The registered run used the tree that is described here.
7.4 Failures found by running against the real toolchain (each has a regression test).
(1) REPL never flushes a pipe -> stdbuf; (2) lake env paths are cwd-relative -> absolutised;
(3) a second import Mathlib in a live REPL costs +3.9 GiB anonymous and tripped the 4 GiB
watchdog on the first multi-case run -> one import per process, layered headers; (4)
#print axioms's collector is private in 4.9 -> own traversal; (5) with autoImplicit on (plain
Lean default) an unknown identifier in a statement is silently an implicit variable, so "invalid
reference statement" needs a genuine type error to trigger reference_invalid; (6) sqrt under
open Real Nat is already ambiguous, so a root-level def sqrt is not a viable definition hole
here (instances and variable are); (7) pool statistics were counted only when an error escaped
acquire, not when the caller handled it.
7.5 Hand mutants (each removes one fix in a COPY of the package, then runs the non-slow
tests; .tmp/lean_notes/mutants.py, final run after the last code change except docs):
| Mutant (fix removed) | Killed by | |
|---|---|---|
| M01 | accept any audit-tagged message (forgeable verdict) | test_audit_message_without_the_nonce_is_ignored_forged_verdict_regression |
| M02 | no axiom whitelist check | test_each_audit_finding_rejects[axiom/sorryax/ofreduce] |
| M03 | ignore the kernel statement bridge | test_each_audit_finding_rejects[bridge] |
| M04 | no meta-baseline subtraction | test_verdict_accepts_a_clean_audit |
| M05 | no meta-declaration check | test_each_audit_finding_rejects[meta] |
| M06 | ignore sorry warnings / sorries |
test_each_audit_finding_rejects[sorrywarn/sorrylist] |
| M07 | header failure scored 0 instead of LeanInfraError |
test_header_failure_raises_infra_error_never_a_zero |
| M08 | candidate runs without the reference env | test_command_order_and_envs_are_the_contract |
| M09 | no stdbuf |
test_wrapped_argv_uses_stdbuf_prlimit_and_nice |
| M10 | kill the pid, not the process group | test_timeout_kills_grandchildren_too_via_process_group |
| M11 | no memory watchdog | test_memory_watchdog_caps_anonymous_memory_not_rss |
| M12 | timeout without killing | test_timeout_kills_the_process_and_leaves_no_zombie |
| M13 | tolerate bytes after the terminator | survives: equivalent mutant (two concatenated JSON objects fail json.loads anyway); the real defence is M39 |
| M14 | first := wins |
test_sig_end_skips_let_in_type_not_the_first_colon_eq |
| M15 | no char-literal handling | test_lexer_char_literal_quote_is_not_a_string_start |
| M16 | block comments do not nest | test_lexer_drops_line_and_nested_block_comments |
| M17 | no raw-scan fallback on lexer anomalies | test_anomaly_triggers_raw_scan_... |
| M18 | re-import for every header variant | test_second_header_variant_reuses_the_import_never_imports_twice_regression |
| M19 | lake paths left cwd-relative | test_build_child_env_absolutises_... |
| M20 | no header equality | test_static_rejections[header...] |
| M21 | set_option whitelist off |
test_banned_constructs_fire[set_option...] |
| M22 | dead pool emits zeros | test_reward_raises_when_the_pool_looks_dead_... |
| M23 | defs accepted as proofs | test_each_audit_finding_rejects[def] |
| M24 | kernel recheck never requested | test_kernel_recheck_is_on_by_default_... |
| M25 | skip_tc ignored |
test_each_audit_finding_rejects[skiptc] |
| M26 | recheck failure ignored | test_each_audit_finding_rejects[recheck] |
| M27 | private/attribute target allowed | test_static_rejections[target_modifier] |
| M28 | signature token equality off | test_static_rejections[statement_mismatch] |
| M29 | identifier ban list off | test_banned_constructs_fire |
| M30 | salvage unclosed fences | test_extract_unclosed_fence_is_not_salvaged |
| M31 | first fence instead of last | test_extract_takes_last_closed_lean_fence_and_ignores_think |
| M32 | duplicate target allowed | test_static_target_declared_twice_is_rejected |
| M33 | ablated verifier usable as a reward | test_reward_refuses_the_ablated_verifier |
| M34 | worker never returned to the pool | hang-killed (the pool tests block; 90 s watchdog) |
| M35 | no recycling after max_requests |
test_worker_recycled_after_max_requests |
| M36 | unbounded glibc arenas | test_build_child_env_absolutises_... |
| M37 | child inherits the whole lake env |
test_build_child_env_absolutises_... (secrets leak assertion) |
| M38 | no output cap | test_oversized_output_kills_the_process |
| M39 | late second answer attributed to the next request | test_late_second_answer_is_detected_... |
| M40 | open Lean makes meta identifiers spellable |
test_banned_constructs_fire[open Lean...] |
40 mutants: 38 killed by an assertion, 1 killed by a hang (M34), 1 survivor (M13, equivalent).
Not covered by any mutant, by construction: the skip_tc audit path against the REAL option (it
does not exist on this pin; test_real_skip_kernel_tc_option_does_not_exist_on_the_pin fails the
day the pin changes) and the Lean prelude's kernel-recheck loop against a proof that elaborated
with the kernel disabled (no way to produce one on 4.9 without the banned meta-programming).
7.2 V1 freeze (2026-10-14, branch phase0/verifier; PROPOSED FROZEN HASH, merge after chain6 exits).
Fixes (regressions in tests/test_lean_hardening.py, each adversarial proof was accepted or aborted a batch before):
U08-1/2 lexer desync (\/ and // are single tokens; a comment opener glued to any other symbol is refused as
ambiguous; numerals no longer swallow letters: 1macro; raw strings of any hash count; real-Lean differential fuzz);
U08-40 s!/f!/m! interpolation flagged whatever sits before the quote; U08-4/12 _align* names and
_root_./«» spellings banned; U08-5 axiom-walk fuel exhaustion reports _align_fuel_exhausted (fails closed) and a
missing axioms field is audit_incomplete; U08-3 ReplPool.from_toolchain(sandbox=True) is the default, fails closed
with SandboxUnavailable, sandbox=False is the explicit opt-out; U08-8 every real REPL runs under the launcher/supervisor
(ReplProcess.supervise) that SIGKILLs it when the parent process dies (measured: orphaned before, reaped now);
U08-6 stale env ids after a worker death raise ReplCrash; U08-7 lone surrogates reject that item only; U08-17 budget
starts after acquire(); U08-18 a bad reference header is reference_invalid, not a batch abort; U08-21 any exception
mid-request kills the child; U08-11(codex) unmeasurable memory fails closed after mem_miss_limit samples; U08-16
timeout/crash/memory/protocol map to Outcome.UNDECIDED (new enum member in align/eval/verifier.py, reward stays 0).
Ported from the red-team session: opt-in independent_recheck (recheck.py), default off.
NOT changed (design choices, math verifier, need a decision): U08-9/10/11/15 (tolerance, texty fallback, unit stripping,
i), U08-13/14/22 (extractor ReDoS/format), U08-19/20 (preflight opt-in, pin not enforced at runtime).
Verification: exploratory ceiling run (2 workers, sandboxed): known-good 176/177 accepted (the one reject is a
179 s timeout under host load), adversarial 0/61 accepted. Registered run to do after the chains exit (needs the heavy
lock): python scripts/lean_ceiling_test.py --workers 8.
Frozen hash: sha256 over, for each align/verify/**/*.py in sorted path order, path + NUL + bytes + NUL:
6df56348db12d8e255427764f994d0f3ab29d4713e84ddda07c9637c31f12648.
7.3 FROZEN (2026-10-19). Merged verifier (V1 + MV math-checker fixes) hash
f1dd9e7871ade3a9dd37587c10a7a17025fe8623a735455ec40206607e120b5c (scripts/p2/verifier_hash.py; supersedes the
7.2 proposal, which predates MV). Registered ceiling run (8 workers, heavy lock, sandboxed, .tmp/restart/ceiling/result.json):
known-good 178/179 accepted = 0.9944 (Wilson95 [0.9690, 0.9990], floor 0.98) PASS; adversarial 0/61 accepted PASS
(a compile-only grader would accept 51). Every SOTA number from here on is verified under this hash; chain8 refuses to
run a step if align/verify changes.
8. Operations
bash scripts/lean_setup.sh # install / repair (idempotent, ~3 min, 5.8 GB, under /apps)
bash scripts/lean_setup.sh --check # exit 0 iff the install is complete
source /apps/development/rlhf/lean/env.sh # only if you want elan/lake in your shell
pytest tests/test_lean_verifier.py -m "not slow" # no Lean needed (fake REPL binary)
pytest tests/test_lean_verifier.py -m slow # real toolchain, 2 workers (~1 min)
python scripts/lean_ceiling_test.py --verify-prereg
python scripts/lean_ceiling_test.py --workers 8 # registered run: preflight + heavy-job lock
python scripts/lean_ceiling_test.py --measure-only # install size, cold/warm import, PSS
ALIGN_LEAN_ROOTrelocates the install. Every cache the toolchain writes is redirected under it bylean_setup.sh; nothing goes to$HOME,/or/tmp.- Worker stderr spools to
<root>/tmp/pool/worker<i>.stderr(truncated per respawn; the tail is quoted inReplCrash). - Before widening the pool:
plan_workersandReplPool.from_toolchain(preflight=True)are the only sanctioned way; never construct more workers than the 45 GB floor allows. - A new Lean/Mathlib pin is a new verifier: re-run the ceiling test, update
PINS.jsonprovenance in Section 1, and regenerate any cached verdicts. - Hand mutants (Section 7) are run on a COPY of the package under
.tmp/mutants/; the repo is never edited in place.