Applications

Stream: new members

[Adolfo Neto]

Are there any good public examples of aplications of Lean in Software Formal Verification?

[Henrik Böving]

I think the most impressive example of software verification in pure Lean 4 that I know about is SATurn by @Siddhartha Gadgil https://github.com/siddhartha-gadgil/Saturn

[Johan Commelin]

There's an MSc student in Utrecht working on a verified wasm compiler in Lean 4. But I'm not sure how public that project is.

[Joachim Breitner]

Could you connect me to him? There is a project to generate all forms of Wasm spec (prose, latex, interpreter, mechanized semantics) from a single source of truth, and I contributed the lean4 backend. A verified compiler should if possible connect to that specification, this would make it compatible with all other Wasm lean formal work that maybe exists in the future.