3 ms·
"Formally-verified"? What exactly, and how? Doesn't seem to be mentioned in the README or anywhere else in the repository.
by ivanbakel 5y ago
"Formally-verified"? What exactly, and how? Doesn't seem to be mentioned in the README or anywhere else in the repository.
- Bootvis 5y agoYou have to dig into the Wiki: > 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.
- _xyy4 5y agoHi, maintainer of the crate The formal verification comes from [fiat-crypto](https://github.com/mit-plv/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.