Please see below for research publications about and using Verus, as well as projects built using Verus. To add your work here, please open a pull request that adds a new file to the 'source/docs/publications-and-projects' directory.

Verus — Publications

Publications by the Verus team

Verus: Verifying Rust Programs using Linear Ghost Types [code]
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel

Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA),
December, 2023
Leaf: Modularity for Temporary Sharing in Separation Logic [code]
Travis Hance, Jon Howell, Oded Padon, and Bryan Parno

Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA),
December, 2023
A Framework for Debugging Automated Program Verification Proofs via Proof Actions [code]
Chanhee Cho, Yi Zhou, Jay Bosamiya, and Bryan Parno

Proceedings of the Conference on Computer Aided Verification (CAV),
July, 2024
Distinguished Paper Award
Verifying Concurrent Systems Code
Travis Hance

PhD Thesis, Carnegie Mellon University,
August, 2024

Beyond Isolation: OS Verification as a Foundation for Correct Applications,
Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, Andrea Lattuada

Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS),
June, 2023
Atmosphere: Towards Practical Verified Kernels in Rust
Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, Anton Burtsev

Proceedings of the Workshop on Kernel Isolation, Safety and Verification (KISV),
October, 2023
Anvil: Verifying Liveness of Cluster Management Controllers [code]
Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, Tianyin Xu

Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI),
July, 2024
Best Paper Award
VeriSMo: A Verified Security Module for Confidential VMs [code]
Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui

Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI),
July, 2024
Best Paper Award

A Distributed Key-Value Store

A port of the IronKV system from IronFleet to Verus. IronKV uses distribution for improved throughput by moving “hot” keys to dedicated machines.
A Concurrent Memory Allocator

A memory allocator based on mimalloc.
A Node Replication (NR) Library

Creates a linearizable NUMA-aware concurrent data structure from a black-box sequential one
An Append-only Log on Persistent Memory

The implementation handles crash consistency, ensuring that even if the process or machine crashes, it acts like an append-only log across the crashes. It also handles bit corruption, detecting if metadata read from persistent memory is corrupted.
An OS Page Table Management Implementation and OS Model

A verified implementation of an OS’ page table management code, and proofs that it behaves according to a userspace process’ expectations when combined with a model of the hardware’s memory management (memory translation) subsystem.
Vest: Verified Parsers and Serializers

High-assurance and performant parsing and serialization of binary data formats.