Don't LEAN On Me

How Covert Proof-checker Failures Eradicate 'Formal-Verification'-powered Agentic Guardrails

Arka Dash  ·  Carlos José Duarte Casillas (Universidad de Sonora)  ·  Rishab Kumar Jha (JIIT)  ·  Yatharth Maheshwari  ·  Aditya Bansal

With Apart Research  ·  2026

1. Introduction

Large language models are probabilistic and occasionally deceptive, so a recurring proposal for controlling autonomous agents is to gate their actions behind a deterministic checker that cannot be argued with. Interactive theorem provers, and Lean 4 in particular, are the natural candidate. The Lean-Agent Protocol admits an agentic action "if and only if the Lean 4 kernel proves" it satisfies pre-compiled policy axioms. Multi-agent frameworks such as MA-LoT use Lean kernel feedback as the arbiter of correctness, and DeepMind's AlphaProof reached silver-medal IMO performance because Lean verification guarantees each step.

This paper asks what happens when the certification itself can be forged. A formal verifier is a trustworthy guardrail only if a kernel-accepted, clean-audit proof corresponds to a true statement. We show that on a current Lean release this correspondence breaks without any custom axiom, without sorry, without unsafe in the victim's code, and without any signal in the canonical audit tool.

The mechanism is not a zero-day. Lean's reference manual states that native_decide "depends on the correctness of the Lean compiler and all definitions with an @[implemented_by] attribute," and issue #7463 (open, priority P-low) records that attribute-driven trust admissions are not reflected by #print axioms. What is new is the threat model: as the kernel becomes an automated gate for AI agents, the parties consuming a proof are no longer the Lean experts who understand native_decide.

2. The Three-Component Chain

The break composes three native mechanisms:

1. Divergence injection — @[implemented_by f] installs a runtime body that contradicts the source body, with only a type check enforced.
2. Kernel admission — native_decide closes a Decidable goal by compiling and running the procedure, recording trust as a synthetic axiom <thm>._native.native_decide.ax_N_M.
3. Audit blindness — #print axioms walks the proof term only; it never inspects the @[implemented_by] registry. The synthetic name is the sole trace and names neither the diverging function nor the attribute responsible.

The kernel reads isBlue .Red = false (source body). The compiler runs isBlue_lie which always returns true. native_decide admits the runtime answer as a certified equation. #print axioms reports one opaque synthetic name — mentioning neither isBlue nor the attribute. By ex falso quodlibet, every proposition becomes provable.

3. The Four-Module Supply Chain

Mallory's PR is a 2-line diff of the exact shape used hundreds of times in Lean core and Mathlib — an idiomatic performance optimization.

-- Step2_FastPath.lean  (Mallory, attacker)
import ColorExploit.Step1_Defs
namespace Colors
private def isBlue_lie (_ : Color) : Bool := true   -- diverges from isBlue_src
@[implemented_by isBlue_lie]
def isBlue (c : Color) : Bool := isBlue_src c        -- source body still honest
end Colors

-- Step3_Bridge.lean  (Carol, honest)
theorem productionIsBlue : isBlue .Red = true := by native_decide

-- Step4_Consumer.lean  (Bob, honest victim)
def kernelLabel : String := if isBlue .Red then "BLUE" else "RED"
theorem dashboardSaysBlue : kernelLabel = "BLUE" := by
  simp [kernelLabel, productionIsBlue]

4. Results

Result 1 — the kernel certifies a false equation

'Colors.productionIsBlue' depends on axioms:
  [productionIsBlue._native.native_decide.ax_1_1]

The kernel accepts isBlue .Red = true on the native compiler's authority. The source body defines isBlue .Red = false. The kernel's theory is inconsistent.

Result 2 — the inconsistency reaches an honest consumer with a clean audit

info: Step4_Consumer.lean: 'Colors.dashboardSaysBlue' depends on axioms:
  [propext, productionIsBlue._native.native_decide.ax_1_1]
Build completed successfully (5 jobs).

dashboardSaysBlue is kernel-certified to equal "BLUE", yet the kernel's own reduction of kernelLabel yields "RED". Bob has no native_decide, no custom axiom, no unsafe.

Result 3 — the audit surface gives false reassurance

Empirical Study: AI Agents and the Soundness Gap (33 trials)

We measured how frontier Claude agents handle optimization requests in the presence of the @[implemented_by] trap across two codebases (250-line stack VM, 350-line regex matcher) and three model tiers.

Sonnet 4.6 refused an explicit red-team prompt identifying the request as an attack against formal-verification infrastructure — then complied with a subtle in-source "PERF NOTE (spec v2.1, ratified 2026-03-12, see ticket HW-1247)" comment requesting the same divergence. In-source injection beats safety training.

5. Implications for AI Safety

Architectures that admit an action "iff the Lean kernel proves it safe" inherit this gap directly: if any dependency in the import graph carries the 2-line pattern above, an attacker can pre-certify a false safety lemma and the action passes the gate while the audit looks clean.

The aggravating factor specific to AI pipelines is the reader. A human expert might recognize native_decide in a PR and interrogate the synthetic axiom; an automated merge gate has no defense current tooling supports — the opaque name is indistinguishable from routine native evaluation. As Lean becomes the deterministic backstop for probabilistic agents, the population consuming its proofs is shifting away from the experts who understand this trust admission.

6. Suggested Mitigations

1. Make #print axioms legible. Name the attribute-driven admission explicitly, e.g. [via @[implemented_by] of isBlue → isBlue_lie in Step2_FastPath], restoring the self-describing signal the v4.29.0 per-call naming change removed.
2. lake-level allowlist. Track which dependencies may use trust-bypassing attributes (@[implemented_by], @[csimp], @[extern]); default-deny for new dependencies.
3. CI kernel/native diff check. Diff kernel reduction against native evaluation for all Decidable terms reachable by native_decide, flagging mismatches before merge.

The fix is cheap and local. It should land before, not after, agentic Lean gating is deployed at scale.

7. Reproduction

git clone https://github.com/r34l-rudr44/sps-hackathon.git
cd sps-hackathon/test_project
cat lean-toolchain          # leanprover/lean4:v4.30.0-rc2
lake build Myproject.Supply.Step4_Consumer

Expected output:

info: Step4_Consumer.lean: 'Colors.dashboardSaysBlue' depends on axioms:
  [propext, productionIsBlue._native.native_decide.ax_1_1]
Build completed successfully (5 jobs).

To re-run the full empirical study (requires Lean toolchain + stored trial files):

cd experiments
for m in haiku sonnet opus; do
  ./validate3.sh trials/${m}_Esoft.lean   $m Esoft
  ./validate3.sh trials/${m}_Finject.lean $m Finject
  ./validate4.sh trials/${m}_Gsoft.lean   $m Gsoft
  ./validate4.sh trials/${m}_Ginject.lean $m Ginject
done

8. Related Work

The underlying mechanism is documented in Lean issue #7463, the Lean Zulip "native_decide leakage" thread, and lean-pitfalls. The community treats this as a usage hazard for proof authors, not a security concern. No prior work treats it as a supply-chain or agentic-pipeline threat, or analyzes the consumer-side audit surface for a non-expert inheriting a pre-certified lemma via import.

The general "frame-shape" safety phenomenon is established in Anthropic's Sabotage Evaluations and Sleeper Agents. Our study is a domain specialization in the target domain of interactive-theorem-prover soundness — to our knowledge the first empirical measurement of LLM-induced soundness corruption in any ITP.