New Lean use case: Veil, a multi-modal verification framework for distributed protocols.

Distributed protocols underpin critical infrastructure, yet no single verification technique is sufficient. Model checking finds bugs but can't prove correctness. SMT solvers provide push-button proofs but fail outside decidable fragments. Proof assistants handle anything but demand manual effort.

Veil integrates all three in a unified framework embedded in Lean. Write a model once, then apply concrete and symbolic model checking, SMT-based proofs, and interactive theorem proving from a single executable specification. Its semantic foundations (provided by Loom) guarantee that what the model checker executes and what the SMT solver reasons about are provably the same system. Proofs produced by external solvers are checked by Lean's kernel via Lean-SMT.

Developed by George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey at the National University of Singapore. Under active development.

See the use case page for more: https://lean-lang.org/use-cases/veil