> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them.

Since both Rust and C have LLVM IR intermediates, you could use KLEE[0] for this.

[0] https://klee-se.org/