projects

• zebra
  An independent Zcash node implementation built in Rust. Production-grade, fully validating, developed at the Zcash Foundation.
  Rust · Zcash · ZcashFoundation
• zcash-p2p-spec
  A TLA+ formal specification of the Zcash peer-to-peer network protocol, following ZIP-0204. Models handshake, keepalive, block sync, and disconnection with full message-passing constraints.
  TLA+ · Formal Methods · Zcash
• crosslink2
  A TLA+ specification of the Crosslink2 hybrid consensus protocol, modeled as a state machine with BC, BFT, and finalization subprotocols. Safety and liveness properties verified via model checking.
  TLA+ · Formal Methods · Consensus
• formal-market-mechanisms
  Formal verification of batch auction market mechanisms. Proving fairness properties of trade execution using mathematical proof techniques.
  TLA+ · Formal Methods
• → more on GitHub
  Full project list on GitHub.