From eb7df8080520b9be6f5696b9eff9293005c4950e Mon Sep 17 00:00:00 2001 From: Michael Rosenberg Date: Mon, 20 Apr 2026 02:03:45 -0400 Subject: [PATCH] Link formal verification results (#899) --- curve25519-dalek/README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/curve25519-dalek/README.md b/curve25519-dalek/README.md index ee64e49..2d902dd 100644 --- a/curve25519-dalek/README.md +++ b/curve25519-dalek/README.md @@ -234,6 +234,17 @@ inappropriate CPU would cause `SIGILL`, but the entire backend is only invoked when the appropriate CPU features are detected at runtime, or when the whole program is compiled with the appropriate `target_feature`s. +## Formal Verification + + + the word 'certified', next to a checkmark + + +A large chunk of `curve25519-dalek` has been formally verified with [Verus](https://verus-lang.github.io/verus/guide/). Specifically, the 280 Rust functions in version 4.1.3 of `curve25519-dalek` that are used directly or indirectly by the Signal Messenger app. For more details on what was verified and with which assumptions, see the VeriLib page [here](https://verilib.org/cert/5132). + # Performance Benchmarks are run using [`criterion.rs`][criterion]: