The issue with SAT/SMT for program verification is it's too much like dark magic. It's acceptable if you can have it generate a proof certificate for the properties you care about and commit these with the Rust source code - but AIUI, generating usable proof certificates for 'unsat' proofs is a hard problem where you might be better off writing out the proof interactively.