Highlights
- Pro
Pinned Loading
-
cargo-vouch
cargo-vouch PublicProve a loop-light Rust function is panic-free auto-generates a Kani proof harness and reports BUG / UNGUARDED / VERIFIED. Never fakes a pass.
Rust
-
clean-poseidon2
clean-poseidon2 PublicMachine-checked soundness for circomlib Poseidon(2) in Lean 4 (cLean) - discharges the poseidon_2 axiom assumed by Veridise's Semaphore v3 verification
Lean
-
epbs-formal
epbs-formal PublicMachine-checked TLA+ formal model of Ethereum ePBS (EIP-7732) for the Glamsterdam upgrade. TLC-verified safety + liveness.
TLA
-
proof-carrying-ai
proof-carrying-ai PublicProof-carrying compliance certificates for AI agent actions: machine-checked (Coq, axiom-free) + zero-knowledge proofs that an agent action obeyed a formal policy.
Python
-
proof-carrying-safety-shield
proof-carrying-safety-shield PublicProof-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
-
qualkit
qualkit PublicPre-flight assurance for quantized conformal models — tells you what compression did to your coverage guarantee before deployment.
Python
If the problem persists, check the GitHub status page or contact support.