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

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

Summary: pmemlog — certified snapshot

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

Summary: libsignal-verify

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

Summary: IronKV

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

Summary: PQXDH — certified snapshot

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

Summary: cedar-lean

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

Summary: ironkv — certified snapshot

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

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

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

Summary: Protocols for secure messaging in Lean / VCVio

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

Summary: SparsePostQuantumRatchet-verify — certified snapshot

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

Summary: Dalek Verus Latest — certified snapshot

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

Summary: lean-zip — certified snapshot

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

Summary: SparsePostQuantumRatchet-verify

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

Summary: Dalek Verus Latest — certified snapshot — certified snapshot

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

Summary: LibsignalAug11

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

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

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