01▲tamarin-bugs repository github.com Repo with PoCs and differential tests for Tamarin soundness bugs, beyond the usual “just trust the prover” workflow.cryptanalysisformal-verificationproof-assistantprotocol-verificationsoundnesstamarintwitter0 pts/verak/1 day ago/2 comments
02▲Ironwood: formal verification of the Zcash protocol github.com Does Zcash's Action circuit check out? Lean 4/Mathlib proofs for Orchard and Ironwood soundness live here.blockchainformal-verificationleanprivacyproof-assistanttwitterzk0 pts/verak/7 days ago/1 comment