Smart Casual Verification of the Confidential Consortium Framework

Learn about a hybrid verification approach called "smart casual verification" applied to the Confidential Consortium Framework (CCF) in this 18-minute conference talk from NSDI '25. Discover how researchers from Azure Research at Microsoft combined formal specification and model checking with automated testing to validate CCF's distributed protocols, including its unique consensus protocol and client consistency model. Explore the integration of TLA+ formal specifications with C++ implementation through a continuous integration pipeline that allows ongoing validation as the codebase evolves. Understand the practical challenges of applying formal verification methods to complex existing codebases and how the team overcame these obstacles to identify six subtle bugs before they could impact Microsoft's Azure Confidential Ledger service in production. Gain insights into making formal verification more accessible and sustainable for real-world distributed systems development beyond traditional one-off expert-driven approaches.