verify_proof exploits

[jxin31415]

verify_proof Limitations

In the interest of scalability, verify_proof trusts the Lean environment to behave correctly. That's usually fine, but a sufficiently creative adversary can exploit this to make invalid proofs appear valid with Lean metaprogramming.

This is a known limitation that we don't expect to address, since the alternatives below cover adversarial use cases.

If you're verifying untrusted code, consider additionally using these other resources which perform a similar check. These run proofs in isolated environments and are less susceptible to known exploits, at the cost of speed:

• lean4checker: Lean FRO-developed .olean verifier
• Comparator: Lean FRO-developed gold standard for proof judges
• SafeVerify: battle-tested public proof checker

We recommend reading the Lean4 reference page on this topic for more discussion.

Example Attack Patterns

Malformed declaration exploit with verify_proof URL