We have a PR to add proofs for ml-kem using Kani: RustCrypto/KEMs#379
Before merging that, I think we should probably pick a common proof system to use across the whole project, so we don't wind up with various proofs in different incompatible proving systems and can focus on a single one.
We have a PR to add proofs for
ml-kemusing Kani: RustCrypto/KEMs#379Before merging that, I think we should probably pick a common proof system to use across the whole project, so we don't wind up with various proofs in different incompatible proving systems and can focus on a single one.