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 (the Lean project in this repo) is licensed under the Apache License, Version 2.0 (LICENSE).

The code under curve25519-dalek/ is vendored (with minimal modifications) from the upstream curve25519-dalek project and is licensed under the BSD-3-Clause license; see curve25519-dalek/LICENSE.