Verified-zkEVMPolyFun

Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols
Displaying 1-4 of 4 packages depending on Verified-zkEVM/PolyFun
Sort by

  1. Verified-zkEVM/Arklibuses3710d71

    Formally Verified Arguments of Knowledge in Lean

  2. proximity-prize/proximity-prizeusesv4.32.2

  3. zksecurity/sigmausescf8b35c

    Formal verification of knowledge soundness for Generalized Bulletproofs

  4. Verified-zkEVM/VCViouses3710d71

    Machine-checked cryptographic proofs in Lean, built on Mathlib: oracle computations, probability semantics, program logic, and lattice- and hash-based schemes.