fiat-crypto 0.2.9 is the machine-generated, formally-verified Rust extraction of the Fiat Cryptography project: field-arithmetic primitives for P-224, P-256, P-384, P-521, Curve25519, secp256k1, p434, and Poly1305. VCS byte-equivalence holds. No unsafe code, no I/O, no build-time execution, no dependencies, and no binary artefacts. No findings. Correctness and constant-time claims are left unasserted; the upstream Coq proofs are the documented correctness evidence.