PropProof: Free Model-Checking Harnesses from PBT

Abstract

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 , a library that automatically converts 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 , an AWS-developed protocol-buffer library with nearly 40 million downloads. is being used in ’s CI. Our evaluation on 42 PBT harnesses from top-ranked open-source Rust libraries demonstrates enabling the use of Kani to verify complex, user-defined properties on existing code with minimal user intervention.