Zulip Chat Archive

Stream: new members

Topic: Applications

Adolfo Neto (Oct 19 2023 at 17:28):

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

Henrik Böving (Oct 19 2023 at 18:48):

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 (Oct 19 2023 at 19:11):

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 (Oct 19 2023 at 19:16):

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.

Last updated: Dec 20 2023 at 11:08 UTC