Verifying transactional database systems

Project overview

The goal of this project is to build and formally verify practical and high-performance transactional database systems, based on the Perennial verification framework. Our OSDI ‘23 vMVCC paper reports on our first step toward the goal: verifying a high-performance transaction library.


vMVCC is a high-performance transaction library with a formal specification and a machine-checked proof of correctness. vMVCC addresses the core technical challenge faced by the transaction layer in a database—correctly and efficiently executing concurrent transactions.

vMVCC adopts multi-version concurrency control (MVCC), a popular technique used in many other research and commercial database systems. MVCC improves concurrency by retaining past versions for readers to read, while allowing writers to add new versions. Formally reasoning about MVCC requires advanced proof techniques, such as logical atomicity and prophecy variables.