Distributed protocols underpin critical infrastructure — from consensus in blockchains to replication in databases — yet they remain notoriously difficult to get right. Bugs emerge from subtle interactions across unbounded numbers of participants, and testing alone is not always sufficient to build confidence. Veil aims to become the tool of choice for building assurance in distributed protocols, integrating symbolic and concrete model checking, SMT-based automated proofs, and interactive theorem proving in a unified framework embedded in Lean.
One-Stop Shop for Protocol Reasoning
No single verification technique is sufficient for distributed protocols. Model checking finds bugs but cannot prove correctness. SMT solvers provide push-button proofs but fail opaquely outside decidable fragments. Proof assistants handle anything but demand manual effort. These techniques are complementary, yet until now, using them together often meant maintaining parallel specifications across separate tools.
Veil's vision is to be a one-stop shop for protocol reasoning: write a model once, then test it with concrete and symbolic model checking, discover an inductive invariant guided by counterexamples, and verify it using whatever combination of automation and interactive proof works best.
Proof Assistant as Platform
Due to its embedding in Lean, Veil has a very small trusted computing base. 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, both derived from a single executable specification, with their agreement proven in Lean. And thanks to Lean-SMT, proofs produced by external solvers are checked by Lean's kernel.
The embedding pays dividends in user experience, too. Veil uses Lean's ProofWidgets to render minimised counterexamples, execution traces, and verification results directly in the IDE. This is the kind of rich, interactive feedback that is painful to build in a standalone tool but comes for free when one builds their verifier in Lean.
We believe this approach generalises beyond protocol verification. As Lean's meta-programming, proof automation, and IDE infrastructure continue to mature, the case for embedding verifiers inside Lean — rather than building them from scratch — only grows stronger. Every improvement to Lean is an improvement to every verifier built on it.
Next Steps
Veil is built for:
-
Protocol engineers who want to test and verify their designs
-
Researchers who want to build on top of a verified multi-modal verification infrastructure
-
Developers curious about formal verification who want a gentle on-ramp
If you are interested: