Post

1/3 New Lean use case: Veil, a multi-modal verification framework for distributed protocols from George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey at NUS.

1/4/26, 3:28 pm4 reposts11 likes

a bezoar

@a-bezoar.bsky.social

1 Apr

verse-lab: Verified Systems Engineering @ NUS verse-lab.org CAV 2025 paper that introduces Veil Veil: A Framework for Automated and Interactive Verification of Transition Systems George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey verse-lab.org/papers/veil-...

verse-lab.orgVERSE LabVerified Systems Engineering @ NUS

Lean Focused Research Organization

@lean-lang.org

1 Apr

2/3 Veil's approach: write a model once, then apply model checking, SMT-based proofs, and interactive theorem proving from a single specification. Its embedding in Lean means a very small trusted computing base.

Lean Focused Research Organization

@lean-lang.org

1 Apr

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-lang.orgLean Programming LanguageLean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.