3/3 "As Lean's meta-programming, proof automation, and IDE infrastructure continue to mature, the case for embedding verifiers inside Lean only grows stronger."
See the use case: lean-lang.org/use-cases/veil
Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.