KEQ proves migrated code behaves exactly like the original, on all inputs — from small C/Rust examples to SHA-256 implementations in OpenSSL and RustCrypto.
