The open-source library for

formally verified code

Showing 1–16 of 1,764
Sort by
Lean
Lean Verified ✓

Summary: Protocols for secure messaging in Lean / VCVio

Repo: https://github.com/Beneficial-AI-Foundation/secure-messaging

Rust
Aeneas Verified ✓

Summary: SparsePostQuantumRatchet-verify — certified snapshot

Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify

Rust
Verus Featured Verified ✓ VeriLib Certified

Summary: Dalek Verus Latest — certified snapshot

Repo: https://github.com/Beneficial-AI-Foundation/dalek-verus

Lean
Lean Featured Verified ✓ VeriLib Certified

Summary: lean-zip — certified snapshot

Repo: https://github.com/kim-em/lean-zip

Rust
Aeneas Featured Verified ✓

Summary: SparsePostQuantumRatchet-verify

Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify

Rust
Verus Featured Verified ✓ VeriLib Certified

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

Repo: https://github.com/Beneficial-AI-Foundation/dalek-verus

Rust
Verus VeriLib Certified

Summary: ironkv — certified snapshot

Repo: https://github.com/verus-lang/verified-ironkv

Rust
Verus Verified ✓ VeriLib Certified

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

Repo: https://github.com/Beneficial-AI-Foundation/dalek-verus

Rust
Verus

Summary: LibsignalAug11

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Verus Verified ✓

Summary: Dalek Verus upload submission - 06/08/2026, 05:48:14 PM

Repo: https://github.com/Beneficial-AI-Foundation/dalek-verus

Rust
Aeneas Verified ✓

Summary: SparsePostQuantumRatchet-verify upload submission - 06/08/2026, 05:48:34 PM

Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify

Lean
Lean Verified ✓

Summary: lean-zip upload submission - 06/08/2026, 05:47:09 PM

Repo: https://github.com/kim-em/lean-zip

Rust
Aeneas Verified ✓

Summary: curve25519-dalek-lean-verify

Repo: https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify

Rust
Aeneas

Summary: libsignal-verify

Repo: https://github.com/Beneficial-AI-Foundation/libsignal-verify

Rust
Dafny

Summary: Testing | small boxes

Repo: https://github.com/signalapp/libsignal/tree/main/rust

Rust
Dafny

Summary: RustSignalMay15Sofia

Repo: https://github.com/signalapp/libsignal/tree/main/rust