We do research in the design and implementation of programming languages, program synthesis, and computer-assisted formal reasoning about complex systems, at the School of Computing of National University of Singapore, as a part of PLSE@NUS lab.
News
Veil has been featured as one of the verification use cases of Lean on the official Lean website!
New post on Proofs and Intuitions: Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory. We describe an experiment in mechanising Move’s borrow checker in Lean with AI assistance, producing 39K lines of metatheory in about 27 working days.
Our paper on grammar repair with examples and tree automata will appear at OOPSLA’26.
New post on Proofs and Intuitions: Verifying Distributed Protocols in Veil. We take a tour of Veil, a Lean-based verification framework that combines TLA+-style model checking with formal proofs and enables AI-powered invariant inference.
We now have a research blog: Proofs and Intuitions. In our first post, we show how to specify and verify imperative programs in Lean using Velvet by combining automated symbolic reasoning with AI-assisted theorem proving.
Linard Arquint joins the team as a Research Fellow. Welcome, Linard!
Two talk proposals are accepted to the Dafny Workshop 2026: (1) on Velvet and (2) on our experience of building Veil in Lean.
Thibault Dardinier joins the team as a short-term Visiting Research Fellow. Welcome, Thibault!
Dipesh Kafle, Yueyang Feng, and Valentin Mikhalchuk join the lab as PhD students. Welcome, Dipesh, Yueyang, and Valentin!
Recent Blog Posts
Research Themes
Most of research done in the lab currently is powered by Lean proof assistant.
Our current investigations follow the themes outlined below. For more details on our research, check out our projects, and recent papers.
Theme 1: Multi-Modal Verification in Lean
Modern software systems are too complex for any single validation technique. We build multi-modal verifiers in Lean that combine fuzz-testing and model checking with deductive proofs—both automated and interactive—across domains including imperative programs, distributed protocols, security protocols, and general-purpose languages. Along the way, we advance methodologies for testing, specification and invariant inference, and both automated and interactive verification.
Our goal is to bridge the gap between system implementations and their abstract models, producing robust, easy-to-maintain proofs.
Theme 2: Program Synthesis with Correctness Guarantees
Program synthesis automatically derives programs from declarative specifications, slashing the effort needed to produce correct-by-construction code. By marrying deductive proofs in proof assistants (Rocq, Lean) with synthesis, we have built tools that generate correct-by-construction implementations for complex tasks in mainstream languages, and that automatically synthesise data structure specifications.
We aim to synthesise provably correct, high-performance, safety-critical programs with low-effort proof automation and evolution.
Theme 3: Verified Foundations of Distributed Systems
Distributed systems power modern computing—from cloud services to blockchains—yet asynchrony, partial failures, and concurrent state transitions make their correctness notoriously hard to establish. We develop mathematical foundations for specifying and verifying distributed protocols, including consensus protocols, Byzantine fault-tolerant systems, and distributed data structures, drawing on automated reasoning, separation logic, fuzz testing, and compositional verification.
Our long-term goal is a verified software stack for distributed computing, where protocol designs ship with machine-checked proofs that carry through to executable implementations.
People
Faculty and Postdocs
Graduate Students
Interns and Research Assistants
Recent Collaborators
Software
Publications
Recent
Grammar Repair with Examples and Tree Automata
41st ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2026). Oakland, CA, USA, October 2026.
Foundational Multi-Modal Program Verifiers
53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). Rennes, France, January 2026.
Velvet: A Multi-Modal Verifier for Effectful Programs
Dafny Workshop 2026 (co-located with POPL 2026). Rennes, France, January 2026.
Lessons from Building an Auto-Active Verifier in Lean
Dafny Workshop 2026 (co-located with POPL 2026). Rennes, France, January 2026.
Inductive Synthesis of Inductive Heap Predicates
40th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2025). Singapore, October 2025.
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
41st International Conference on Logic Programming (ICLP 2025). Rende, Italy, September 2025.
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
34th USENIX Security Symposium. Seattle, WA, USA, August 2025.
Veil: A Framework for Automated and Interactive Verification of Transition Systems
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
Accelerating Automated Program Verifiers by Automatic Proof Localization
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
Concurrent Data Structures Made Easy
39th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2024). Pasadena, CA, USA, October 2024.
Join Us
PhD Positions: We are actively looking for motivated PhD students (although the number of available positions in the team is limited to 1-2 per year)! Get in touch with Ilya Sergey if you want to chat about research opportunities, and apply here.
Research Internships: If you are interested in a research internship with us, please get in touch with your CV and a paragraph of text describing your specific interests in the research themes we pursue at the moment. Strong background in PL/logic/verification or systems-building is a must. Prospective internship candidates will have to complete a test verification task in Lean.
