Property-based testing (PBT) is often used by Rust developers to test functional correctness properties of their code. Since PBT uses randomized testing, its guarantees are limited: it can detect bugs but provides no formal guarantees of correctness. The Kani Rust Verifier uses the CProver verification framework to verify Rust code, given a specification in a Kani verification harness. However, developers must manually write Kani harnesses while avoiding model-checking-specific pitfalls like large memory usage or
timeouts.

We introduce propproof, a library that automatically converts proptest PBT harnesses into Kani harnesses which can be formally validated using Kani. We discuss the data-structure models we developed in order to optimize performance of these Kani verification harnesses. Using this library, we identified and fixed 2 issues in PROST, an AWS-developed protocol-buffer library with nearly 40 million downloads. propproof is being used in PROST’s CI. Our evaluation on 42 PBT harnesses from top-ranked open-source Rust libraries demonstrates propproof enabling the use of Kani to verify complex, user-defined properties on existing code with minimal user intervention.