Skip to content
@Verified-zkEVM

Verified zk(E)VM

Github organization for the verified zk(E)VM formal verification project

Popular repositories Loading

  1. ArkLib ArkLib Public

    Formally Verified Arguments of Knowledge in Lean

    Lean 348 124

  2. clean clean Public

    Lean circuit DSL

    Lean 207 34

  3. VCVio VCVio Public

    A Lean library for machine-checked cryptographic proofs.

    Lean 169 58

  4. evm-asm evm-asm Public

    Lean 59 14

  5. CompPoly CompPoly Public

    Computable Polynomials in Lean.

    Lean 49 45

  6. PolyFun PolyFun Public

    Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols

    Lean 18 5

Repositories

Showing 10 of 18 repositories
  • leanerVM Public

    Lean 4 implementation and formalization of leanVM

    Verified-zkEVM/leanerVM's past year of commit activity
    Lean 4 2 13 21 Updated Nov 2, 2026
  • ArkLib Public

    Formally Verified Arguments of Knowledge in Lean

    Verified-zkEVM/ArkLib's past year of commit activity
    Lean 348 Apache-2.0 124 14 28 Updated Nov 2, 2026
  • VCVio Public

    A Lean library for machine-checked cryptographic proofs.

    Verified-zkEVM/VCVio's past year of commit activity
    Lean 169 Apache-2.0 58 17 52 Updated Nov 2, 2026
  • CompPoly Public

    Computable Polynomials in Lean.

    Verified-zkEVM/CompPoly's past year of commit activity
    Lean 49 Apache-2.0 45 6 (1 issue needs help) 9 Updated Nov 2, 2026
  • PolyFun Public

    Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols

    Verified-zkEVM/PolyFun's past year of commit activity
    Lean 18 Apache-2.0 5 9 20 Updated Nov 2, 2026
  • evm-asm Public
    Verified-zkEVM/evm-asm's past year of commit activity
    Lean 59 MIT 14 150 (1 issue needs help) 6 Updated Nov 2, 2026
  • clean Public

    Lean circuit DSL

    Verified-zkEVM/clean's past year of commit activity
    Lean 207 MIT 34 37 32 Updated Nov 2, 2026
  • riscv-zkvm Public

    Lean extraction of the Sail RISC-V specification for verified zkVM projects

    Verified-zkEVM/riscv-zkvm's past year of commit activity
    Lean 13 4 2 74 Updated Nov 2, 2026
  • Foxglove Public

    A formalisation of Foxglove, a modification of the Bluebell probabilistic program logic (See https://arxiv.org/pdf/2402.18708), adapted to functional programs in Iris-lean.

    Verified-zkEVM/Foxglove's past year of commit activity
    Lean 1 Apache-2.0 0 0 0 Updated Oct 27, 2026
  • hash-specs Public
    Verified-zkEVM/hash-specs's past year of commit activity
    Lean 0 0 0 0 Updated Oct 27, 2026
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Lean OCaml TeX