Summary: Anderson-Conjecture
Repo: https://github.com/frenzymath/Anderson-Conjecture.git
Summary: A library for certified numerical reasoning that turns floating-point suggestions into machine-checked theorems over the reals.
Repo: https://github.com/alerad/leancert
Summary: A formally verified reimplementation of the Lean 4 kernel in pure Lean 4, with accompanying metatheory
Repo: https://github.com/digama0/lean4lean
Summary: SPQR
Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify
Summary: dalek-verus
Repo: https://github.com/Beneficial-AI-Foundation/dalek-verus
Summary: SparsePostQuantumRatchet-verify upload submission - 06/08/2026, 05:48:34 PM — certified snapshot
Repo: https://github.com/Beneficial-AI-Foundation/SparsePostQuantumRatchet-verify
Summary: KVAC-model
Repo: https://github.com/Beneficial-AI-Foundation/KeyedVerificationAnonymousCredential-model
Summary: secure-messaging
Repo: https://github.com/Beneficial-AI-Foundation/secure-messaging
Summary: cedar-lean
Repo: https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean
Summary: curve25519-dalek-lean
Repo: https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify
Summary: ironkv
Repo: https://github.com/Beneficial-AI-Foundation/verified-ironkv/tree/main/ironsht
Summary: IronKV
Repo: https://github.com/verus-lang/verified-ironkv/tree/main/ironsht
Summary: Protocols for secure messaging in Lean / VCVio
Repo: https://github.com/Beneficial-AI-Foundation/secure-messaging
