Hacker News new | past | comments | ask | show | jobs | submit login
Orion 0.17 – X25519 with formally-verified field arithmetic and serde support (github.com/orion-rs)
43 points by todsacerdoti 4 days ago | hide | past | favorite | 3 comments

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact