Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent System
summary
IronSync is an automated verification framework that uses an ownership type system and a Localized Transition System to split global proofs into small, mechanized shards. It verifies linearizability and data safety by proving implementations refine shard-level transitions, then lifting those to a global state machine. Case studies reimplement a SplinterDB page cache and NROS node replication into verified, executable artifacts, find a linearizability bug, report proof ratios of 5:1 and 7:1, ~15 minutes verification time, and performance within 9% of originals.
AI-written summary · about
chapters (5)
related talks
20mFine Grained Replicated State Machines for a Cluster Storage System
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
01h 30mImplementing, verifying and debugging distributed event-based systems
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
39mTrust Deterministic Execution to Scale & Simplify Your Systems
15mQuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
25mProperty-agnostic base case extension for scalable verification of distributed systems
31mPractical Smart Contract Sharding with Ownership and Commutativity Analysis