Union-Find and Usability: A Verification Case Study
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 a union-find implementation within the E-graphs project, egg. I found that while Prusti was more user-friendly in terms of UI, Creusot made it easier to verify more complex properties.