Realistic Rust Verification for Software Engineers
Are automated Rust verifiers usable by programmers without a formal methods background? At LLNL, I conducted a case study using the Prusti and Creusot formal verification tools. Both tools were used to verify the correctness of the underlying union-find of the E-graphs, egg. I found that while Prusti was more user-friendly in terms of UI, Creusot made it easier to verify more complex properties.