Crux, a Precise Verifier for Rust and Other Languages
Stuart Pernsteiner, Iavor S. Diatchki, Robert Dockins, Mike Dodds, Joe, Hendrix, Tristan Ravich, Patrick Redmond, Ryan Scott, Aaron Tomb

TL;DR
Crux is a verification tool that enables precise, cross-language analysis of complex code, such as cryptographic modules, by translating Rust and C code into symbolic tests for correctness verification.
Contribution
Crux introduces a new framework for cross-language verification, especially for Rust, using symbolic unit tests and compositional reasoning to verify complex code modules.
Findings
Successfully verified SHA1 and SHA2 implementations in Rust.
Supports both inline properties and extensional equality checks.
Operates effectively in production environments, including industry use.
Abstract
We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is designed for use in production environments, and has already seen use in industry. In this paper, we focus on Crux-MIR, our verification tool for Rust. Crux-MIR provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust. Notably, Crux-MIR supports compositional reasoning, which is necessary to scale to even moderately complex…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHorticultural and Viticultural Research
