Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026New York

TCB-Expansion Attacks on Lean 4 and the LLM Proof Reviewers That (Mostly) Miss Them

Juliet Meza · Team 501st Lean-gion

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: TCB-Expansion Attacks on Lean 4 and the LLM Proof Reviewers That (Mostly) Miss Them

Open in a new tab (opens in new tab)
Presentation

Presentation: TCB-Expansion Attacks on Lean 4 and the LLM Proof Reviewers That (Mostly) Miss Them

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

Using an open Lean bug (#7463), I built 23 proofs that the kernel accepts as valid but are actually false. The attack works by smuggling a fake axiom through a @[csimp] rewrite, which native_decide then compiles and runs — without the kernel ever seeing it. Lean's own audit command, #print axioms, reports the proof as clean. There is no warning, no flag, and nothing visually different from an honest proof.

I then tested whether three LLMs (Claude Opus, Sonnet 4.6, GPT-4o) could catch these attacks acting as proof reviewers. The short answer: they catch what they can see, and miss what they can't. When the attack is in the same file, models reject it 35 out of 36 times. When it is hidden in an imported module, they can't catch it without tool access. Give them tools and they walk the import chain themselves and find it. A secondary finding: GPT-4o can be socially engineered. Embedding a fake audit approval note in the Lean file's docstring caused GPT-4o to accept 6 out of 12 attacks. Claude models flagged the fake note as a prompt injection attempt every time.

The fix is a 7-layer defensive stack, anchored by two new tools: a static scanner and a recursive auditor that finds the axioms #print axioms hides.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. The project successfully demonstrates a critical vulnerability in Lean 4's trusted computing base (TCB) by exploiting issue #7463, where '@[csimp]' lemmas can smuggle false axioms that bypass '#print axioms'. The author constructs a dataset of 23 adversarial Lean 4 files and evaluates LLM proofreaders on this dataset, revealing cross-model heterogeneity in detecting prompt injection via Lean docstrings. The recursive '#print axioms' auditor effectively closes the #7463 vector, and the static scanner flags critical patterns. However, the project's scope is limited to a single version of Lean 4, and the dataset size is relatively small, which may limit its generalizability.

    The main weakness lies in the limited scope and sample size, as well as the reliance on a specific version of Lean 4. The findings are based on a small set of attacks (23 files), and the cross-model heterogeneity results are derived from only 12 trials per cell. Additionally, the project does not explore potential bypasses or defenses in other versions of Lean 4 or other proof assistants, which could provide a more comprehensive understanding of the issue.

    To strengthen the findings, the author should conduct a cross-toolchain regression test to ensure that the attacks and defenses are effective across different versions of Lean 4. Additionally, expanding the dataset size would provide stronger empirical evidence for the claims made. Broadening the scope to include other proof assistants with similar escape hatches could also enhance the project's impact.

    Read full reviewShow less

  2. Great idea to home in on a specific bug in Lean and explore it's potential for vulnerability. The two angles (reproducible attacks and recursive audit tool) are impressive contribution for the sprint. Questions I'd have for next: (a) how does Lean manage the risk and how could your patch lead to a PR; (b) is there an experiment that shows this vulnerability leading to reward hacking in RLVR?

Cite this project

@misc{meza2026tcbexpansion,
  title = {{TCB-Expansion Attacks on Lean 4 and the LLM Proof Reviewers That (Mostly) Miss Them}},
  author = {Juliet Meza},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/tcbexpansion-attacks-on-lean-4-and-the-llm-proof-reviewers-that-mostly-miss-them-o3hn}},
  url = {https://apartresearch.com/sprints/projects/tcbexpansion-attacks-on-lean-4-and-the-llm-proof-reviewers-that-mostly-miss-them-o3hn}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026