Many of the verification and static analysis tools we build at Galois are based on the same technology: a symbolic execution engine for a language called Crucible. There are a lot of advantages to doing this. It’s what makes it possible for SAW to reason about C, C++, Rust, and x86 assembly, all through the same interface, just by translating into Crucible. Improvements to Crucible improve all our tools at once, and the systems we’ve verified form a natural test set that helps us avoid bugs and performance regressions. Crucible also makes it much easier to build new tools. For instance, Galois recently announced Crux, a verification tool based on symbolic testing. A user of Crux can write a test harness with symbolic inputs and then check whether assertions in the test case could ever fail. Behind the scenes, Crux translates programs to Crucible. This works great for sequential programs, but it made us wonder whether we could use the same technology to build a simple verifier for multi-threaded Rust programs. It turns out that Crucible makes that pretty easy! Let’s take a look at what we did. Let’s examine the following simple program: fn inc(val: u32) -> u32 {    if val == u32::MAX { val } else { val + 1 } } fn dec(val: u32) -> u32 {    if val == 0 { val } else { val - 1 } } fn action(do_inc: bool, value: u32) -> u32 {    if do_inc { inc(value) } else { dec(value) } } We might want to check that if we chain action three times, then the difference between the resulting value and the original value is no more than 3. We can devise the following test in crux-mir (the Rust version of Crux) to check this is the case for an arbitrary starting value and an arbitrary sequence of three actions: #[cfg_attr(crux, crux_test)] fn test() {    let v0 = u32::symbolic(&qu