IronSpec - Increasing the Reliability of Formal Specifications

Explore a 15-minute conference talk from USENIX OSDI '24 that introduces IronSpec, a groundbreaking framework designed to enhance the reliability of formal specifications in verified systems. Delve into the challenges of ensuring the correctness of specifications and discover how IronSpec adapts classical software testing practices to address this critical issue. Learn about the framework's innovative features, including automated sanity checking, SpecTesting Proofs (STPs), and automated spec mutation testing. Examine the results of IronSpec's evaluation on 14 specifications, including six from real-world verified codebases, and uncover how it successfully identified ten specification bugs across these systems. Gain insights into the importance of robust specifications in maintaining the integrity of formally verified systems and how IronSpec contributes to strengthening the foundations of software verification.