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
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!
Our paper on using Answer Set Programming for invariant inference will appear at ICLP’25.
Our paper on accelerating SMT-based program verifiers will appear at CAV’25.
A paper on synthesising Separation Logic predicates via Answer Set Programming is accepted at OOPSLA’25.
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
Given the importance of modern software systems (e.g., distributed systems, concurrency and high-performance computing libraries, etc) and their complexity, it is vital in industry to have a rigorous methodology that combines both lightweight validation techniques, such as fuzz-testing and model checking with deductive proofs, both automated and human-assisted. Reasoning tools that provide the full spectrum of such validation methodologies are referred to as multi-modal verifiers. In this line of work, we are focusing on building multi-modal verifiers for different kinds of domains (including imperative programs, distributed protocols, security protocols, and general-purpose languages) on top of Lean proof assistant, advancing the state of the art in methodlogies for testing, specification and invariant inference, as well automated and interactive program verification.
We aim to build verification tools that bridge the gap between the systems implementations and their abstract models that can be verified in an interactive or automated fashion, producing robust and easy-to-maintain proofs.
Theme 2: Program Synthesis with Correctness Guarantees
Program synthesis is an emerging research and technology paradigm for automatically deriving programs from user-provided declarative specifications, thereby significantly reducing the implementation effort required for producing correct-by-construction and efficient code. Our recent work explored the marriage of state-of-the-art techniques for deductive proofs in a proof assistants (e.g., Coq and Lean) and program synthesis that resulted in a series of tools that produce correct-by construction implementations for complex tasks in mainstream languages, as well as approaches for automatically synthesisng data structure specifications.
Our long-term agenda targets synthesis of provably correct high-performance, safety-critical programs with the focus on low-effort proof automation and evolution.
Theme 3: Verified Foundations of Distributed Systems
Distributed systems form the backbone of modern computing infrastructure, from cloud services to blockchain protocols, yet their correctness remains notoriously difficult to establish due to the inherent complexity of asynchrony, partial failures, and concurr ent state transitions. Our research focuses on developing rigorous mathematical foundations for specifying and verifying distributed protocols, relating runnable implementations to well-understood models and their compositions. This work includes verified implementations of consensus protocols, Byzantine fault-tolerant systems, and distributed data structures, building on techniques from automated reasoning, separation logic, fuzz testing, and compositional verification to enable modular proofs that scale to realistic system complexity.
Our long-term goal is to build a verified software stack for distributed computing, where protocol designs come equipped with machine-checked correctness proofs that carry through to executable implementations, closing the gap between abstract protocols and deployed systems.
People
Faculty and Postdocs
Graduate Students
Interns and Research Assistants
Recent Collaborators
Software
Publications
Recent
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.
DSLs in Racket: You Want It How, Now?
17th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’24). 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.
