Issues

• Tracking: repository layout and consolidation

  Verified-zkEVM/VCVio#1150 · Filter by author dtumad opened on Nov 13, 2026

• VCVioFrontier: the cslib-frontier side of VCVio

  Verified-zkEVM/VCVio#1149 · Filter by author dtumad opened on Nov 13, 2026

• Tracking: Lean v4.36 bump

  Verified-zkEVM/VCVio#1148 · Filter by author dtumad opened on Nov 13, 2026
  1

• Rust interop: the state of the hax and Aeneas bridges, and coordination with hax-lean

  Verified-zkEVM/VCVio#1093 · Filter by author dtumad opened on Nov 12, 2026
  2

• Tracking: generic results from DeepMind's Signal verification

  Verified-zkEVM/VCVio#1086 · Filter by author quangvdao opened on Nov 11, 2026

• Tracking: remove the last four sorrys and enforce zero sorry debt

  Verified-zkEVM/VCVio#1008 · Filter by author dtumad opened on Oct 30, 2026

• ML-DSA EUF-CMA at FIPS 204 parameters: the assumptions the proved headlines still take

  Verified-zkEVM/VCVio#995 · Filter by author dtumad opened on Oct 30, 2026
  1

• Remaining quantum random-oracle results: classical embedding, shared games, oracle checks and compressed-oracle bounds

  Verified-zkEVM/VCVio#966 · Filter by author quangvdao opened on Oct 28, 2026

• Quantum reductions as signature morphisms, and gate-level cost

  Verified-zkEVM/VCVio#965 · Filter by author quangvdao opened on Oct 28, 2026

• Quantum programs: loops, coherent port choice, implementation access and path expansions

  Verified-zkEVM/VCVio#964 · Filter by author quangvdao opened on Oct 28, 2026

• Tracking: computational complexity (PPT definition, complexitylib backend, adequacy)

  enhancement
  Verified-zkEVM/VCVio#906 · Filter by author dtumad opened on Oct 22, 2026
  1

• feat(Cryptol): coordinate whole-Foundation import and direct VCVio comparisons

  Verified-zkEVM/VCVio#879 · Filter by author dtumad opened on Oct 19, 2026
  1

• Tracking: generic and algebraic group models (GGM and AGM)

  enhancement
  Verified-zkEVM/VCVio#846 · Filter by author quangvdao opened on Oct 12, 2026
  5

• Naming conventions for security notions (adversary, experiment, game, advantage)

  Verified-zkEVM/VCVio#801 · Filter by author quangvdao opened on Sep 23, 2026
  3

• Restate and prove Fujisaki–Okamoto and ML-KEM security (replaces #189–#191, #213–#215)

  Verified-zkEVM/VCVio#785 · Filter by author quangvdao opened on Sep 22, 2026
  1

• UC follow-ups from the PolyFun UC audit (HasPlugFactorization, quotient semantics, graded observations, non-vacuous OTP)

  Verified-zkEVM/VCVio#633 · Filter by author dtumad opened on Sep 3, 2026
  2

• SLH-DSA follow-ups from the stack reviews: F/T1 separation, reduction-checklist items, doc nits

  Verified-zkEVM/VCVio#629 · Filter by author alexanderlhicks opened on Sep 2, 2026
  2

• Definition & Security Proofs for Merkle Trees

  Verified-zkEVM/VCVio#571 · Filter by author BoltonBailey opened on Aug 28, 2026
  5

• Design and roadmap: Mathlib-aligned denotational probability semantics

  enhancement
  Verified-zkEVM/VCVio#532 · Filter by author dtumad opened on Aug 21, 2026
  13

  

• Proposal: hash-based post-quantum signature lane (Generalized XMSS / leanSig) over the existing TweakableHash

  Verified-zkEVM/VCVio#505 · Filter by author Abraxas1010 opened on Jul 28, 2026

• Untracked proof obligations in the GPV / Falcon / Rényi chain (gaps from #187, #279)

  proof wanted
  Verified-zkEVM/VCVio#396 · Filter by author dtumad opened on May 14, 2026
  2

• Proof obligation for MLDSA.euf_cma_security in LatticeCrypto/MLDSA/Security.lean

  proof wanted
  Verified-zkEVM/VCVio#228 · Filter by author quangvdao opened on Apr 1, 2026
  3