Associate Professor Ilya Sergey and Team Win Distinguished Paper Award at CAV 2026

A research group at NUS Computing has received a Distinguished Paper Award at CAV 2026, one of the flagship conferences on formal methods and verification, for their work on Velvet, a tool that automatically proves whether a piece of code does what it’s meant to do. CAV 2026 was held as part of FLoC 2026, the 9th Federated Logic Conference.

The paper, “Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean” was one of eight papers to receive the award, out of 81 accepted submissions and 311 papers submitted overall. The team is led by Associate Prof Ilya Sergey, together with Vladimir Gladshtein, a final-year PhD student and the paper's lead author, fellow NUS Computing PhD students Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, and Vitaly Kurin.

Proving Code Does What It’s Supposed to Do 

Testing a program only reveals how it behaves on the inputs someone happened to try. Velvet takes a different route, known as formal verification. Developers write a precise statement, alongside their code, describing what that code is supposed to do, and Velvet builds a mathematical proof that the code satisfies it across every possible input. It works on ordinary imperative programs, the kind most real-world software is written in, with mutable variables, loops, and exceptions.

Verification tools already exist. Dafny is one; Verus, used at Amazon AWS, Google, and Microsoft, is another. Prof Sergey's team points to two recurring frustrations with these tools. Automation that fails offers little recourse beyond reworking the code and hoping for a different outcome. And the verifiers themselves are substantial pieces of software, which means trusting the tool becomes almost as important as trusting the code it's checking.

"For decades, every program verifier has been its own island, with its own language, its own logic, and its own bugs. Our bet is that verifiers should instead be ordinary libraries inside a single proof assistant, where they can share specifications, decades of formalised mathematics, and the rapidly improving AI automation growing around Lean,” said Assoc Prof Sergey. “Velvet shows this recipe can produce a tool that matches industrial verifiers while being trustworthy down to a tiny proof-checking kernel. The award is encouragement that the community sees promise in this direction. The credit goes to the people who built Velvet: Vladimir Gladshtein, a final-year PhD student who led the effort, Vitaly Kurin, who started on it as an intern and is now joining us as a PhD student, and the rest of the VERSE Lab team, who together pushed Lean well past what it was thought to be for.”

Building a Verifier Inside a Proof Assistant

Velvet is built as a library inside Lean, the proof assistant mathematicians use to formalise research mathematics and now a leading platform for AI-driven theorem proving. Most proofs are generated automatically. Where automation runs out, developers can open the proof, see exactly what remains unproven, and finish it themselves using Lean's tactics, its Mathlib library, or AI assistance. Lean's small trusted kernel checks every proof regardless of how it was produced, so confidence in the result doesn't depend on trusting Velvet's own code.

Since the CAV 2026 paper was published, Prof Sergey says Velvet is now ten times faster than the version reported at the conference, and that it now outperforms Dafny, whose automation is considered the state of the art in automated verification. Velvet extends a broader research programme in VERSE Lab building a family of domain-specific verifiers as Lean libraries on shared foundations. An earlier tool, Veil, verifies distributed protocols and was published at CAV 2025. The work was partially supported by a Singapore Ministry of Education Tier 3 grant and a Stellar Development Foundation Academic Research Grant.

Velvet is open source, available at https://github.com/verse-lab/velvet.

What's Next

The team has two directions in mind. One treats Velvet as a form of computer-checked pseudocode. Researchers have long used pseudocode to communicate algorithms concisely, but without any guarantee that the pseudocode itself is correct. A Velvet program can serve the same purpose while carrying a machine-checked proof, opening a path toward AI-assisted algorithm discovery, where an AI proposes candidate programs, Lean checks them, and only the correct ones survive. LeetProof, a first step in this direction, is due to appear at ASE'26.

The other is teaching. As students increasingly write code with AI assistance, Prof Sergey argues that the skill worth building is learning to state precisely what a program should do. They plan to bring Velvet into the classroom, giving students immediate, rigorous feedback on whether their programs meet their own specifications.