Feature Proposal: Lean 4 proof export backend for hevm

[MavenRain]

Summary

I'd like to propose adding a Lean 4 proof export backend to hevm that translates symbolic execution traces into machine-checkable proof obligations. I have a pending EF ESP grant for this work and wanted to gauge maintainer interest before proceeding.

Motivation

When hevm's SMT solver returns "unsatisfiable" for a property, the result is ephemeral. There is no persistent, auditable artifact that a third party can independently check. For high-value contracts, this gap matters.

A proof export backend would:

1. Translate symbolic execution paths into Lean 4 theorem statements
2. Automatically generate Lean 4 proofs for properties hevm fully verifies
3. Produce partial proof skeletons (with explicit sorry gaps) for properties that exceed hevm's bounds

Scope

The proposed work is designed as a modular addition to minimize maintenance burden:

• Trace extraction module: A new module exporting symbolic execution traces (path conditions, storage transitions, branch metadata) as a structured IR (JSON or S-expressions). This is the only part that touches hevm's Haskell codebase.
• External translation tool: A standalone tool converting the IR to Lean 4 proof obligations. Lives outside hevm's repo.
• Lean 4 libraries: EVM semantics library and tactic library for automated proof generation. Also external.

Questions for maintainers

1. Is this a direction you'd be open to seeing for hevm?
2. Would you be willing to review/merge a trace export module PR, assuming it's well-scoped and doesn't affect existing functionality?
3. Are there any architectural preferences for how trace export should hook into hevm's internals?
4. Are there other efforts in this direction I should be aware of?

Full proposal available on request. Thanks for your time.

[msooseth]

Hi @MavenRain

First of all, thanks for the interest! I am truly happy you have taken the time to look at hevm and come up with an interesting plan. Let me try to write a few words regarding the plan you wrote above. Firstly, it is important to note that I am only ONE of the maintainers, so please keep that in mind reading the below.

In my opinion, we already have an IR, called Expr, so perhaps much of what needs to be done that touches hevm can be minimized/non-existent. Regarding the translation, I don't quite understand what you mean. You mean that your tool will take the IR (i.e. Expr) as correct, and then try to prove that each Expr End is UNSAT? If that is the case, then I think your system may be solving the problem that is less of an issue right now. In my opinion there are three issues that need solving:

1. The Expr End generated may be wrong. This is because our symbolic execution engine may have bugs, e.g. incorrect rewrite rules, or may misinterpret the EVM.
2. The EVM symbolic execution system is currently severely limited, e.g. it cannot deal with unknown code. Hence, many symbolic execution paths stop half-way through and emit a Partial Expr End, effectively signalling that we cannot tell what may happen in this execution path. This happens a lot with real-world contracts due to call to unknown code.
3. The SMT solver cannot solve a dispatched query, or its result is not trustworthy -- although the latter is being worked on by many SMT solver teams by means of emitting a proof trace that can be verified.

Your proposal, if I understand correctly, is focussed on (3)? If my understanding is correct, and indeed you are focussed on (3) then I think, while it is interesting, currently it's the least problematic part of our system. Most dispatched queries are solveable, at least once we apply some new simplifications that are typically not too hard to add. Fixing (1) is something that would be nice, but likely also not extremely odious, as a differential fuzzer should be able to do it, and we indeed have a differential fuzzer like that (though it does need some TLC). In my personal opinion, the most important issue to deal with currently is (2). In my opinion it's the issue that limits hevm the most. If (2) was improved (it likely never be "fixed"), I believe hevm could gather widespread adoption. Improving/fixing (3), is I believe not a high priority right now, although could be of interest, of course, but in my opinion, not the most important issue with hevm.

Again I'd like to note that this is only my opinion, and of course I may have misunderstood your proposed work and it is not attempting at solving (3). Please let me know what you think,

Mate

[MavenRain]

Hi @MavenRain

First of all, thanks for the interest! I am truly happy you have taken the time to look at hevm and come up with an interesting plan. Let me try to write a few words regarding the plan you wrote above. Firstly, it is important to note that I am only ONE of the maintainers, so please keep that in mind reading the below.

In my opinion, we already have an IR, called Expr, so perhaps much of what needs to be done that touches hevm can be minimized/non-existent. Regarding the translation, I don't quite understand what you mean. You mean that your tool will take the IR (i.e. Expr) as correct, and then try to prove that each Expr End is UNSAT? If that is the case, then I think your system may be solving the problem that is less of an issue right now. In my opinion there are three issues that need solving:

1. The Expr End generated may be wrong. This is because our symbolic execution engine may have bugs, e.g. incorrect rewrite rules, or may misinterpret the EVM.
2. The EVM symbolic execution system is currently severely limited, e.g. it cannot deal with unknown code. Hence, many symbolic execution paths stop half-way through and emit a Partial Expr End, effectively signalling that we cannot tell what may happen in this execution path. This happens a lot with real-world contracts due to call to unknown code.
3. The SMT solver cannot solve a dispatched query, or its result is not trustworthy -- although the latter is being worked on by many SMT solver teams by means of emitting a proof trace that can be verified.

Your proposal, if I understand correctly, is focussed on (3)? If my understanding is correct, and indeed you are focussed on (3) then I think, while it is interesting, currently it's the least problematic part of our system. Most dispatched queries are solveable, at least once we apply some new simplifications that are typically not too hard to add. Fixing (1) is something that would be nice, but likely also not extremely odious, as a differential fuzzer should be able to do it, and we indeed have a differential fuzzer like that (though it does need some TLC). In my personal opinion, the most important issue to deal with currently is (2). In my opinion it's the issue that limits hevm the most. If (2) was improved (it likely never be "fixed"), I believe hevm could gather widespread adoption. Improving/fixing (3), is I believe not a high priority right now, although could be of interest, of course, but in my opinion, not the most important issue with hevm.

Again I'd like to note that this is only my opinion, and of course I may have misunderstood your proposed work and it is not attempting at solving (3). Please let me know what you think,

Mate

Hey Mate, I very much appreciate the extent to which you've engaged with my proposal so far. It is encouraging to me! Also, thanks for clarifying some of the taxonomy for me, both here, and in our conversation over Matrix.

In fact, my proposal speaks to #1 and not #3. I don't mean to replace the SMT solver, but to build an independent reference semantics in Lean 4 and prove hevm output is correct with respect to that independent semantics. This would allow for catching buggy refactors in hevm leading to Lean 4 proofs failing to close.

With that said, I acknowledge that #2 is probably the biggest bottleneck, which, in this work, the Lean 4 "sorry gaps" would serve to indicate. The sorry gaps would serve as useful pointers for auditing. In other words, a formal EVM semantics in Lean 4 could serve as a regression oracle for hevm development.

I'm in agreement that leveraging Expr is the correct starting point, and I am confident that my proposed trace extraction module could serialize Expr trees directly rather than via an additional IR.