Verified-zkEVMPolyFun

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

  1. Verified-zkEVM/Arklibuses4181c82

    Formally Verified Arguments of Knowledge in Lean

  2. katzenpost/cryptlibusesc0c9236

    Lean cryptography library for prototyping/modeling protocols and proving protocol properties.

  3. proximity-prize/proximity-prizeuses3710d71

  4. zksecurity/sigmausescf8b35c

    Formal verification of knowledge soundness for Generalized Bulletproofs

  5. Verified-zkEVM/VCViouses4181c82

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