Verify curve25519-dalek

Appearance

Function Status ​

This table shows the verification status of all functions in the project. Click on a function to see more details.

Total:194
Extracted:194
Verified:191
Spec only:0
AI Proveable:16
Function ▲ Rust Source Extracted Verified Issue Notes
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/curve_models/mod.rs✓✓—
backend/serial/scalar_mul/variable_base.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/constants.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/field.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—🤖🏆🌈🎉⭐
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/serial/u64/scalar.rs✓✓—
backend/mod.rs✓✓—
constants.rs✓✓—
constants.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓☐—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
edwards.rs✓✓—
Show columns:

Extracted

✓Rust code has been extracted to Lean
☐Extraction pending

Verified

✓Function has been formally verified
📋Formal specifications but no proofs
✏️Natural language specifications
☐No verification work completed yet