"Formally-verified"? What exactly, and how? Doesn't seem to be mentioned in the README or anywhere else in the repository.

You 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.

Hi, maintainer of the crate

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.