Verse Lab Logo
Verified Systems Engineering @ NUS
Building trustworthy safety-critical systems and advancing the state of the art in formal verification

About Us

Group photo

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.

Announcements

We are actively looking for motivated PhD students! Get in touch with Ilya Sergey if you want to chat about research opportunities, and apply here.

Research internships: In case if you are interested in an 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.

News

25 May 25

Our paper on accelerating SMT-based program verifiers will appear at CAV’25.

14 Apr 25

We are excited to release Veil, a new framework for verifying distributed protocols both automatically and interactively, in Lean! The accompanying paper will appear at CAV’25.

21 Feb 25
25 Jan 25

A paper on programming language synthesis for automated exploit generation is accepted at USENIX Security’25.

09 Jan 25

Congratulations to Yunjeong Lee and Ziyi Yang on receiving Research Achievement Awards!

01 Sep 24
30 Aug 24

Kiran Gopinathan has successfully defended her PhD thesis “Scaling the Evolution of Verified Software”. Congratulations, Dr. Gopinathan!

27 Aug 24

Two new papers at upcoming conferences in October 2024: on compositional verification of Byzantine protocols (CCS’24) and on building concurrent data structures via batch-parallelism (OOPSLA’24).

06 Aug 24

Congratulations to George Pîrlea on receiving a Dean’s Research Excellence Award for 2024!

12 Jul 24

Research Themes

Most of research done in the lab for now 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: Verified Software Systems

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 verification methodology for establishing their correctness properties as well as for making sure that the once completed proofs don’t go “bit rot”. In this line of work, our recent work has introduced logical foundations for compositional verification of complex distributed protocols using a proof assistant. We have also produced the first mechanically verified proof of safety of Nakamoto consensus, its probabilistic properties and verified libraries of relevant probabilistic data structures. We also explored techniques for both foundational and lightweight verification of distributed systems. Finally, we have developed the first approach for (mostly) automated evolution of proofs for verified libraries.

Our long-term goal is 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: Foundations of Verified Program Generation

Often, it is not easy capture an intent of a program synthesis task with a specification that can be also used to formally verify that the synthesised program is indeed correct. In our recent work we started to approach instances of program synthesis with such “intuitive but tricky to make formal” specifications, including generation of sparse data manipulations and automated exploit discovery, from the perspective of program logics.

Our vision in this line of work is to push the state of the art in what can be specified and synthesised, by developing expressive formalisms that capture the program synthesis intent and allow one to mechanically verify its result, interactively or automatically.

People

Faculty

Ilya Sergey
Ilya Sergey
Associate Professor

Graduate Students

Vladimir Gladshtein
Vladimir Gladshtein
PhD Student
Yunjeong Lee
Yunjeong Lee
PhD Student
Yuxi Ling
Yuxi Ling
PhD Student
George Pîrlea
George Pîrlea
PhD Student
Ziyi Yang
Ziyi Yang
PhD Student
Qiyuan Zhao
Qiyuan Zhao
PhD Student

Interns and Visiting Researchers

Gokul Rajiv
Gokul Rajiv
Research Assistant
Valentin Mikhalchuk
Valentin Mikhalchuk
Research Intern

Recent Collaborators

Willow Ahrens
Willow Ahrens
Georgia Institute of Technology
Saman Amarasinghe
Saman Amarasinghe
Massachusetts Institute of Technology
Zhendong Ang
Zhendong Ang
National University of Singapore
Andreea Costea
Andreea Costea
TU Delft
Jonáš Fiala
Jonáš Fiala
ETH Zurich
Matthew Flatt
Matthew Flatt
University of Utah
Seth Gilbert
Seth Gilbert
National University of Singapore
Umang Mathur
Umang Mathur
National University of Singapore
Peter Müller
Peter Müller
ETH Zurich
Nadia Polikarpova
Nadia Polikarpova
UC San Diego
Alex Potanin
Alex Potanin
Australian National University

Projects

Veil

A framework for verifying distributed systems automatically and interactive in Lean

Splean

A simple Separation Logic in Lean

LeanSSR

An SSReflect-Like Tactic Language for Lean

OBatcher

A Multicore OCaml library for batch-parallel data structures

Bythos

A Coq framework for verifying Byzantine Fault Tolerant protocols

LGTM

A hyperlogic for verifying sparse tensor manipulations

Sisyphus

Mostly automated proof repair for verified OCaml functions

SuSLik

Synthesis of heap-manipulating programs from specifications in Separation Logic

ego

An OCaml library that provides generic equality saturation using EGraphs

Ceramist

Verified hash-based approximate membership structures.

Toychain

A Coq implementation of a minimalistic blockchain-based consensus protocol

DiSeL

Mechanised Separation Logic for Compositional Verification of Distributed Protocols

Publications

Recent

Inductive Synthesis of Inductive Heap Predicates

Ziyi Yang and Ilya Sergey

40th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2025). Singapore, October 2024.

Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis

Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, and Ilya Sergey

34th USENIX Security Symposium. Seattle, WA, USA, August 2025.

Veil: A Framework for Automated and Interactive Verification of Transition Systems

George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey

37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.

PDF Code Artefact

Accelerating Automated Program Verifiers by Automatic Proof Localization

Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, and Ilya Sergey

37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.

Concurrent Data Structures Made Easy

Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, and Ilya Sergey

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?

Yunjeong Lee, Kiran Gopinathan, Ziyi Yang, Matthew Flatt, and Ilya Sergey

17th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’24). Pasadena, CA, USA, October 2024.

Compositional Verification of Composite Byzantine Protocols

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

31st ACM Conference on Computer and Communications Security (CCS 2024). Salt Lake City, UT, USA, October 2024.

PDF Code Artefact

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin

38th European Conference on Object-Oriented Programming (ECOOP 2024). Vienna, Austria, September 2024.

Scaling the Evolution of Verified Software

Kiran Gopinathan

PhD Thesis. NUS School of Computing, August 2024.

Mechanised Hypersafety Proofs about Structured Data

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024). Copenhagen, Denmark, June 2024.

VERSE
Verified Systems Engineering
NUS School of Computing