PolyXOR128: a fast Rust universal hash with a Lean-formalized collision bound
PolyXOR128 is a keyed, 128-bit universal hash aimed at fast integrity checks and related constructions. Its author formalized the stated collision-probability bound in Lean and reports high throughput on modern CPUs. This is not a general-purpose cryptographic hash: the guarantee assumes a random secret key independent of the input, the key must remain secret, and the project says it has not had third-party cryptanalysis. It also warns against using the implementation when security is paramount.
The r/rust thread dug into those limits rather than treating the speed claim as a blanket win. Readers debated what “cryptographic strength” means here and flagged benchmark comparability; the author clarified the keyed-hash threat model and added benchmark details, while a separate commenter reported favorable results on an M2.