Building an SMT backend for Lean4

Stream: new members

[Romain Soulat]

Hi everyone!

I'm Romain Soulat, I work at Input Output Global on smart contract verification for the Cardano blockchain. With my team, we're trying to formalize as much as possible of the blockchain, the smart-contract VM, the languages, etc. in Lean 4 so that we can prove correctness properties of real-world smart contracts.

As part of this effort, we’ve built an SMT backend for Lean 4 so that users (hopefully) don’t need to be formal verification experts to use the tool, and so that we can provide counterexamples to help developers debug faster. It’s available here:
https://github.com/input-output-hk/Lean-blaster

We’re currently benchmarking it against existing automation such as smt, auto, aesop, grind, hammer, etc. So far, we’ve tried it on some of the Lean “games” (Natural Number Game, Set Theory Game, Intro to Logic).

Are there any well-known or recommended benchmark suites we could compare against (for example, standard collections of Lean files or goals used to evaluate proof search/automation)? Any pointers or suggestions would be very welcome!

[Niels Voss]

Does this perform proof reconstruction, or does it trust the SMT solver like some other formal verification languages do?

A lot of people will test tactics by using TryAtEachStep, which runs the tactic after every tactic in mathlib

[Romain Soulat]

Right now it trusts both the simplification & normalization step and the smt solver. We’re working on building proof reconstruction for both.