Project to formally verify Dalek elliptic curve cryptography
A project to formally verify the Rust implementation of curve25519-dalek using Lean and Aeneas.
Contributing
Please see CONTRIBUTING.md.
Code of Conduct
We follow the Rust Code of Conduct, with the following additional clauses:
- We respect the rights to privacy and anonymity for contributors and people in the community. If someone wishes to contribute under a pseudonym different to their primary identity, that wish is to be respected by all contributors.
License
The code from curve25519-dalek (contained here within the folder curve25519-dalek) is licensed under either of
- Apache License, Version 2.0, LICENSE-APACHE,
- MIT license (LICENSE-MIT).
See individual files for full information.
The verification code, i.e., the Lean project contained within the repo, is licensed under Apache License, Version 2.0, LICENSE-APACHE.