Coursera Spring Sale
40% Off Coursera Plus Annual!
Grab it
Learn about novel verification techniques for ensuring storage system integrity through this 18-minute conference presentation from OSDI '25. Discover PoWER (Preconditions on Writes Enforcing Recoverability), a groundbreaking approach to verifying crash consistency that encodes requirements in storage API method preconditions, and explore a new media corruption model for provable corruption detection across any storage device type. Examine how these tool-agnostic verification methods rely only on standard constructs like Hoare logic, ghost variables, and quantifiers that most verification tools natively support, eliminating the complexity of previous formal verification approaches. See practical implementations through two verified storage systems: CapybaraKV (a key-value store built with Verus) and CapybaraNS (a notary server built with Dafny), both designed for persistent memory environments. Understand the unique challenges persistent memory presents to building resilient storage systems and learn about innovative solutions including the corruption-detecting Boolean primitive for atomic checksum updates. Gain insights into how both systems achieve verification in under a minute while maintaining competitive performance with similar unverified persistent memory key-value stores, demonstrating the practical viability of formal verification for critical storage infrastructure.
