Formally Verifying
Dalek Elliptic Curve Cryptography

Project to formally verify the Rust code of curve25519-dalek using Verus

84
Specified Functions
43
Fully Verified
16.7%
0
External Functions
0
Axioms

Verification Progress

Verification Funnel
Proof Completion Rate 51.2% 43 of 84 specs are fully proven
Time Period Calculating... Loading tracking data

Counts Over Time

Absolute Counts

Module Breakdown

Module Breakdown

📋 Function Status Data

CSV Preview

Click image to browse all 607 functions. Download CSV →

About the Project

🎯 Project Goals

Formally verify the Rust implementation of curve25519-dalek, a critical cryptographic library used in secure communications worldwide. Our verification uses Verus, a modern verification system designed for Rust.

🔧 What is Verus?

Verus is a tool for verifying the correctness of code written in Rust. It extends Rust with specification constructs and uses automated theorem proving to verify that implementations match their specifications.

🚀 Why This Matters

Curve25519-dalek is used by Signal, Tor, and many other security-critical applications. Formal verification provides mathematical proof that the cryptographic operations are implemented correctly, eliminating entire classes of bugs.

📚 Key Features

  • Formal specifications for cryptographic operations
  • Machine-checked proofs of correctness
  • Continuous integration with verification checks
  • Transparent progress tracking

Getting Started

To run verification locally:

git clone https://github.com/Beneficial-AI-Foundation/dalek-lite.git
cd dalek-lite
cargo verus verify

See the setup instructions for detailed installation steps.

Trust Model

What we need to trust in order to trust these proofs

🛡️

Verus Verifier

We trust that the Verus verification system correctly implements its verification logic and sound reasoning principles.

🔍

Z3 SMT Solver

Verus relies on the Z3 automated theorem prover for checking logical conditions. We trust Z3's implementation of SMT solving algorithms.

🦀

Rust Compiler

We trust that the Rust compiler correctly translates our verified code into machine instructions, and that it respects the semantics Verus reasons about.

📝

Specifications

We trust that our formal specifications accurately capture the intended behavior of the cryptographic operations.

💻

Hardware

Like all software, we ultimately trust that the hardware correctly executes the compiled machine code.

🔐

Cryptographic Assumptions

We trust the mathematical foundations of elliptic curve cryptography, including the hardness of the discrete logarithm problem on Curve25519.

⚠️ What Verification Does NOT Cover

  • Side-channel attacks (timing, power analysis, etc.)
  • Hardware faults or random bit flips
  • Cryptographic assumptions (e.g., DLP hardness)
  • Bugs in unverified dependencies or system libraries

On-Chain Certifications

Verification attestations recorded on the Ethereum blockchain

🔗 Blockchain Attestations

Each verification run produces a JSON with results. The hash of this JSON is recorded on both Ethereum Mainnet (via Gnosis Safe) and Sepolia testnet for transparency and immutability.

📜 What Gets Certified?

  • Verification results JSON (content hash)
  • Commit hash of verified code
  • Number of verified functions
  • Link to downloadable artifact

📋 Certification History

Date Commit Verus Verified Content Hash Mainnet Tx Sepolia Tx Artifact
Loading certifications...

Loading certification data...

Contributing

Help us verify critical cryptographic code

🤝 How to Contribute

We welcome contributions! Whether you're experienced with formal verification or just learning, there are ways to help:

  • Add specifications to unverified functions
  • Complete proofs for existing specifications
  • Improve documentation
  • Report issues or suggest improvements
View Style Guide

📖 Resources