Verus: A Practical Foundation for Systems Verification
Case Studies

• 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.