Veil 2.0 released: verify distributed protocols in Lean 4 with 2–20x faster model checking
tianyin_xu · x · 2026-11-07
Ilya Sergey's team released Veil 2.0, a framework for specifying, model checking, and proving safety and liveness properties of distributed protocols and transition systems in Lean 4.
Key updates:
- Newly verified model checkers for safety, 2–20x faster than TLC, plus liveness support with an LTL proof mode
- A TLA+ → Veil LLM skill for AI coding agents to port existing specs, and a PlusCal-style DSL
- Built-in counterexample-to-induction (CTI) invariant discovery and automatic synthesis via UPDR, with traces and counterexamples visualized in the Lean InfoView
A Playground and GitHub repo are available; work by @zqy1018 and external contributors.
More from coding & agent
- 3/4 of Designers Now Work in Coding Agents, So Proto Is Building a Designer's IDE — antimatter15 · 2026-11-07
- MCP server operators on agent identity: per-IP rate limits break, accounts are the real gate — zach-benson · 2026-11-07
- The 'first mate' pattern: users want one coordinator agent to manage their multi-agent fleets — generativist · 2026-11-07
- Temper open-source repo: a verified runtime for systems that agents build — JoshPurtell · 2026-11-07
- Temper: a verified runtime letting agents build state machines for monitoring — JoshPurtell · 2026-11-07
- json-render/chat: open-source Generative UI letting agents reply with native cards in Slack and Teams — johnlindquist · 2026-11-07