Pinned Loading

1. cargo-vouch cargo-vouch Public

   Prove a loop-light Rust function is panic-free auto-generates a Kani proof harness and reports BUG / UNGUARDED / VERIFIED. Never fakes a pass.

   Rust 1

2. clean-poseidon2 clean-poseidon2 Public

   Machine-checked soundness for circomlib Poseidon(2) in Lean 4 (cLean) - discharges the poseidon_2 axiom assumed by Veridise's Semaphore v3 verification

   Lean 1

3. epbs-formal epbs-formal Public

   Machine-checked TLA+ formal model of Ethereum ePBS (EIP-7732) for the Glamsterdam upgrade. TLC-verified safety + liveness.

   TLA 1

4. proof-carrying-ai proof-carrying-ai Public

   Proof-carrying compliance certificates for AI agent actions: machine-checked (Coq, axiom-free) + zero-knowledge proofs that an agent action obeyed a formal policy.

   Python 1

5. proof-carrying-safety-shield proof-carrying-safety-shield Public

   Proof-carrying safety shield for autonomous systems: z3-verified runtime gate that proves each command safe under bounded disturbance and emits independently-verifiable, forgery-resistant certifica…

   Python 1

6. qualkit qualkit Public

   Pre-flight assurance for quantized conformal models — tells you what compression did to your coverage guarantee before deployment.

   Python 1