A Refinement Methodology for Distributed Programs in Rust

Learn a novel bottom-up refinement methodology for developing verified distributed systems in Rust through this 14-minute conference presentation from OOPSLA 2025. Explore how researchers from ETH Zurich address the limitations of existing refinement techniques by introducing a flexible approach that combines guarded transition systems with locally inductive invariants. Discover how this methodology overcomes the performance issues of top-down refinement and the structural restrictions of traditional bottom-up refinement approaches. Examine the integration of this methodology as a Rust library that leverages the type system for ownership reasoning about guards, enabling verification with standard Rust tools. Study practical applications through substantial case studies, including a concurrent implementation of Memcached, demonstrating the methodology's effectiveness for real-world distributed systems development. Understand how locally inductive invariants provide greater flexibility than standard coupling invariants, supporting diverse program structures, data representations, and proof architectures for verified system development.