Verify Dalek elliptic curve cryptography using Lean

A project to formally verify curve25519-dalek, a Rust implementation of elliptic curve cryptography. The formal verification uses Lean and relies on the Lean representation of the Rust code produced by Aeneas.

Maintainers: Oliver Butterley & The Beneficial AI Foundation

Contributing

See CONTRIBUTING.md.

Project status

See status.md and the Project Site for full details.

Project workflow, verification trust model and repo structure

See details.md.

Code of Conduct

We follow the Rust Code of Conduct, with the following additional clause:

• 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 verification code, i.e., the Lean project contained within the repo, is licensed under Apache License, Version 2.0, LICENSE-APACHE.

The code from curve25519-dalek (contained here within the folder curve25519-dalek with some minimal modifications) is licensed under either of

• Apache License, Version 2.0, LICENSE-APACHE,
• MIT license (LICENSE-MIT).

See individual files for full information.