Sounds like KLEE, but implemented for Rust MIR instead of LLVM IR.
It does. KLEE itself was one of best developments I found. One thing about it with potential for KLEE and this tool is using it for equivalence checks between optimizations in the compiler for a medium-assurance, certifying compiler. Alternatively, testing for breakage during refactoring.