Formally verifyingDalek elliptic curve cryptography

This project aims to formally verify the curve25519-dalek Rust library using the Lean theorem prover. We use Aeneas to automatically extract Rust code into Lean, then we write formal specifications and proofs to ensure the cryptographic implementations are mathematically correct and free from bugs.

We aim to:

• Demonstrate the viability of verifying Rust cryptographic code using Lean
• Develop techniques to make Rust-to-Lean verification more accessible
• Create a resource for learning verification of real-world Rust code

See the project repo or project description for further details.