AI is great at converting C++ to Rust but how can we trust the result? Testing isn't complete enough and human review can't keep up anymore. Often not even the PR author can fully stands behind their generated code. What can we do?
This talk will present a novel method for determistically generating scripts that allow us to prove a Rust rewrite matches C++ implementation using Software analysis workbench and Z3. We will discuss how saw-spec-gen derives constraints and generates mocks for external depencies based on the type system which reduces the overhead. This talk will discuss how these tools are used at Microsoft to prove properties of the metadata security protocol (MSP).
We will discuss the benefits and limitations of implementation verification with SAT solving as well as briefly touch on other formal verification techniques. Formal verification isn't just PhD's anymore! You'll leave with something you can use today.
