The formal verification comes from [fiat-crypto](https://github.com/mit-plv/fiat-crypto), which generates the Rust code of the underlying Curve25519 field arithmetic. Correctness is checked by Coq.
Mention of fiat-crypto was included in the original posts on Reddit/Lobste.rs but seems it was missed in this cross-post.
3 comments
[ 5.4 ms ] story [ 21.6 ms ] thread> Formally-verified crypto
> orion uses the formally-verified field arithmetic generated by fiat-crypto, for the underlying Curve25519 operations.
But the README has a big fat use at your own risk warning so that should probably take precedence.
The formal verification comes from [fiat-crypto](https://github.com/mit-plv/fiat-crypto), which generates the Rust code of the underlying Curve25519 field arithmetic. Correctness is checked by Coq.
Mention of fiat-crypto was included in the original posts on Reddit/Lobste.rs but seems it was missed in this cross-post.