The open-source library for

formally verified code

Showing 1–16 of 1,783
Sort by
Rust
Aeneas Verified ✓

Summary: curve25519-dalek-lean-verify

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

Rust
Aeneas Verified ✓ VeriLib Certified

Summary: SparsePostQuantumRatchet-verify — certified snapshot

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

Lean
Lean Verified ✓

Summary: RogersRamanujan

Repo: https://github.com/AxiomMath/RogersRamanujan.git

Lean
Lean Verified ✓

Summary: Erdos1196

Repo: https://github.com/math-inc/Erdos1196.git

Lean
Lean Verified ✓

Summary: Anderson-Conjecture

Repo: https://github.com/frenzymath/Anderson-Conjecture.git

Lean
Lean Verified ✓

Summary: Leancert

Repo: https://github.com/alerad/leancert

Lean
Lean Featured Verified ✓

Summary: Lean4Lean — verified Lean kernel

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

Lean
Lean Verified ✓

Summary: PQXDH

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

Rust
Aeneas Verified ✓

Summary: SPQR

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

Verus
Verus Verified ✓

Summary: dalek-verus

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

Rust
Aeneas Verified ✓ VeriLib Certified

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

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

Lean
Lean

Summary: KVAC-model

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

Lean
Lean Featured Verified ✓

Summary: secure-messaging

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

Lean
Lean Featured Verified ✓

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