saymrwulf/curve25519-dalek-source
1
0
Fork 0
mirror of https://github.com/saymrwulf/curve25519-dalek-source.git synced 2026-09-07 20:50:39 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Link formal verification results (#899)

Browse source
This commit is contained in:
Michael Rosenberg 2026-04-20 02:03:45 -04:00 committed by GitHub
parent fc23dd4a86
commit eb7df80805
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
curve25519-dalek/README.md
View file

@ -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 invoked when the appropriate CPU features are detected at runtime, or
when the whole program is compiled with the appropriate `target_feature`s. when the whole program is compiled with the appropriate `target_feature`s.
## Formal Verification
<a href="https://verilib.org/cert/5132">
<img
alt="the word 'certified', next to a checkmark"
width="100px"
src="https://verilib.org/assets/img/Badge%20-%20Wide-4x.png"/>
</a>
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 # Performance
Benchmarks are run using [`criterion.rs`][criterion]: Benchmarks are run using [`criterion.rs`][criterion]: