The open-source library for

formally verified code

Showing 1–16 of 1,773
Sort by
Lean
Lean

Summary: PQXDH

Repo: https://github.com/Beneficial-AI-Foundation/PQXDH

Rust
Aeneas Verified ✓

Summary: SPQR

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

Rust
Verus Verified ✓

Summary: dalek-verus

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

Lean
Lean

Summary: KVAC-model

Repo: https://github.com/Beneficial-AI-Foundation/KeyedVerificationAnonymousCredential-model

Lean
Lean Featured

Summary: secure-messaging

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

Lean
Lean Featured

Summary: PQXDH

Repo: https://github.com/Beneficial-AI-Foundation/PQXDH

Lean
Lean

Summary: cedar-lean

Repo: https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean

Rust
Aeneas Featured Verified ✓

Summary: curve25519-dalek-lean

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

Rust
Verus Featured Verified ✓

Summary: ironkv

Repo: https://github.com/Beneficial-AI-Foundation/verified-ironkv/tree/main/ironsht

Rust
Verus

Summary: IronKV

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

Lean
Lean

Summary: Lean 4 kernel / 'external checker' written in Lean 4

Repo: https://github.com/digama0/lean4lean

Lean
Lean

Summary: Protocols for secure messaging in Lean / VCVio

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

Rust
Verus Verified ✓ VeriLib Certified

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

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

Rust
Aeneas Verified ✓

Summary: SparsePostQuantumRatchet-verify — certified snapshot

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

Rust
Verus Verified ✓ VeriLib Certified

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

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