Debug, Execute, Verify! Development-Verification Co-Design Made Practical

To formally verify large-scale systems, development and verification needs to be tightly integrated right from the start but this requires tool support that is currently missing. We present a framework for the Rust programming language that utilizes symbolic program execution to bridge the gap between development and verification. A use case provides first evidence that our tool integrates formal verification into the early development cycle and thus has the potential to scale for the verification of large systems.