The open-source library for

formally verified code

Showing 33–48 of 1,793
Sort by
Rust
Aeneas Verified ✓

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

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

Rust
Verus Verified ✓

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

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

Lean
Lean Verified ✓

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

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

Lean
Lean Verified ✓

Summary: A zero-knowledge Lean4 compiler and kernel

Repo: https://github.com/argumentcomputer/yatima

Rust
Verus Verified ✓

Summary: dalek-verusTestSofia

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

Lean
Lean Verified ✓

Summary: lean-zip

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

Lean
Lean Verified ✓

Summary: Arklib

Repo: https://github.com/Verified-zkEVM/ArkLib

Rust
Aeneas

Summary: spqr-verify with probe-aeneas 0.9.5

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

Lean
Lean

Summary: nasa jpl test — certified snapshot

Repo: https://github.com/nasa-jpl/L4YAML

Lean
Lean

Summary: nasa jpl test

Repo: https://github.com/nasa-jpl/L4YAML

Rust
Aeneas

Summary: SL_PD_Lib

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

Rust
Aeneas

Summary: curve25519-dalek-lean-verify

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

Rust
Aeneas Featured Verified ✓

Summary: SparsePostQuantumRatchet-verify

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

Rust
Verus Featured Verified ✓ VeriLib Certified

Summary: pmemlog — certified snapshot

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

Lean
Lean VeriLib Certified

Summary: PQXDH — certified snapshot

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

Rust
Verus VeriLib Certified

Summary: ironkv — certified snapshot

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