The VERSE Lab in Singapore built the tools that might solve for formal verification at scale.
One of the hardest problems in formal verification has never been mathematics. Proving software correctly traditionally demanded that engineers abandon their languages and habits for the austere world of proof assistants, or trust push-button tools whose automation worked until, opaquely, it didn’t. The gap between those two worlds, full manual proof and full automation, is where most attempts to bring verification into ordinary software engineering have stalled.
A pair of tools from the VERSE Lab at the National University of Singapore, led by the verification researcher Ilya Sergey, represents one of the most credible recent attempts to close that gap. Both were built inside Lean, the proof-oriented programming language created by Leonardo de Moura that has already transformed how mathematics is checked.
Veil: proving the protocols that run everything
Distributed protocols, the algorithms by which fleets of machines agree on a shared state, are among the most consequential and least forgiving artifacts in computing. They underpin databases, payment networks, and blockchains, and their bugs are notoriously subtle: they emerge only in rare interleavings of messages and failures that testing almost never reaches.
Veil, presented at CAV 2025 by George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Sergey, is a framework for verifying such protocols, embedded in Lean 4, that aims to deliver the best of both worlds: push-button automated verification where the logic permits it, and the full power of a modern interactive proof assistant where it does not.
Earlier protocol verifiers forced a choice: fully automatic tools confined users to restricted logical fragments, while fully manual proof assistants demanded expertise few engineering teams possessed. Veil’s thesis was that the two can be layered, with a model checker to find bugs quickly, SMT-solver automation to discharge the routine obligations, and interactive Lean proof for the genuinely hard remainder.
The lab’s recent work adds a further layer that would have sounded fanciful five years ago: AI-powered invariant inference, in which machine learning proposes the key inductive facts that make a protocol’s proof go through, with every suggestion still checked, mechanically and unforgivingly, by Lean itself.
Velvet: proof for the programs engineers write
If Veil addresses the exotic end of software, Velvet addresses the everyday end. Released by the VERSE Lab in late 2025 on top of its Loom framework and spun out as a standalone Lean library in early 2026, Velvet is a verifier for imperative programs, the loops, arrays, and mutable state of ordinary code, that lets an engineer annotate a program with a specification of what it should do and then discharge the proof through a combination of methods.
Sergey describes the approach as multi-modal: the same program and specification can be executed, tested, verified automatically by SMT solvers, and, where automation falls short, proven interactively with Lean tactics, with Lean’s newer automation such as grind and aesop picking up the goals the solvers leave behind.
Two properties distinguish Velvet from the long lineage of program verifiers it descends from. First, it is foundational: the verifier itself is proven sound, so trust bottoms out in Lean’s small logical kernel rather than in a large unverified tool. Second, it lives inside a mainstream proof ecosystem rather than beside one, meaning verified programs, the libraries of Mathlib, and the growing formal computer-science corpus of CSLib all inhabit the same logical world. The work was recognized as a Distinguished Paper at CAV 2026, students have already won a prize at the VerifyThis verification competition using it, and Sergey now teaches with these libraries: his graduate verification course at NUS runs on Veil and Velvet.
Why these tools matter now
Sergey’s Veil and Velvet have arrived at precisely the moment formal verification is shifting from a specialist discipline into a practical necessity. Through the Infinitude Foundation, the investor and philanthropist Chris Hsu, founder of Kilometre Capital and Rocketeer Management, supports scalable formal-verification work through grantees including the Lean Focused Research Organization. Hsu and other frontier innovation specialists are making the argument that AI has pushed formal methods across an economic inflection: the human labor of specification and proof, long the binding constraint, is falling away just as AI-generated code floods into production faster than humans can review it.
The lab’s own output is evidence of that shift. In March 2026, Sergey used an AI coding assistant to mechanize the metatheory of the Move language’s borrow checker in Lean, producing 39,000 lines of formalization in roughly 27 working days, work that would previously have consumed months or years. By August he was describing the change in the field itself: publication-quality verification research now lands in weeks, and the competitive expectations of the discipline are being reset accordingly.
Hsu has argued that convergence is what makes Sergey’s work particularly consequential. AI creates both sides of the equation: it generates and probes software at a scale human engineers cannot match, while also supplying the automation that can make rigorous verification practical at comparable scale. Veil and Velvet provide the crucial bridge between that automation and mathematical certainty. AI can propose invariants, specifications, and proofs; Lean checks the result. The objective is not to make AI infallible, but to make its fallibility irrelevant to what ultimately gets certified.
Veil and Velvet are exactly the kind of tools Hsu’s thesis predicts: automation, increasingly powered by AI, does the work at scale, while Lean’s machine-checked kernel ensures that correctness is never taken on trust.
That architecture, AI proposes and Lean disposes, may be the most important pattern in the two tools. A recurring worry about AI-assisted engineering is that it produces plausible artifacts at a scale no one can review. Verification inverts the worry: an AI can propose invariants, proofs, or translations as creatively and fallibly as it likes, because nothing counts until the proof checker accepts it. The AI contributes speed; the kernel contributes trust.
Hsu has pointed out that sober caveats apply, and the tools’ own authors are the first to recognize them. Velvet remains under active development, and its automated modes, like all SMT-based verification, guarantee conformance to the specification as written; whether the specification captures what the engineer actually meant remains a human responsibility. The lab has put a number on that risk: testing specifications rather than programs, its researchers found underspecification in roughly one in ten of the machine-generated specifications drawn from major Lean benchmarks.
Distributed-protocol proofs in Veil verify designs, and a verified design can still be implemented incorrectly, which is why the surrounding ecosystem, from CSLib’s verified libraries to ongoing work on verified compilation, matters to the endgame. But the direction is unmistakable. Verification is migrating from an esoteric specialty toward an engineer’s toolkit, one Lean library at a time, and the researchers building that migration, in Singapore and elsewhere, are hoping to assemble the working machinery of a future in which proof is simply part of how software gets made.
From software we trust to software we prove
The larger significance of Veil and Velvet, Hsu maintains, is therefore not any single verification technique. They are pieces of an emerging stack in which Lean supplies the trusted foundation, CSLib builds shared computer-science knowledge on top of it, and tools such as Veil and Velvet bring proof into the protocols and programs engineers actually build. That layering is now explicit in the field’s own plans: CSLib’s founding paper names the VERSE Lab’s Loom framework, the substrate beneath Velvet, as infrastructure it will build on. AI increasingly supplies the labor that once made this architecture prohibitively expensive; the proof checker supplies the certainty that AI itself cannot.
That is the broader thesis Infinitude’s Hsu has been advancing: AI is simultaneously making conventional software assurance less adequate and formal verification more practical. As machines write more of the code on which economies, infrastructure, and eventually autonomous systems depend, testing and human review alone become progressively harder to scale. The consequential shift is from asking whether software probably works to establishing mathematically what it cannot do. If that transition succeeds, formal verification will cease to be a specialist safeguard for exceptional systems and become part of the basic and scaled trust infrastructure of an AI-written world.
