All issues

Search results

Reduction.append_completeness is sorried — the single blocker for composed completeness (child of #676)

Status: Open.

#802 In Verified-zkEVM/ArkLib;

· ErVinuelas opened on Aug 26, 2026

BCIKS20 Claim 5.7 (exists_factors_with_large_common_root_set) is missing the eq. (5.3) largeness premise on #S

Status: Open.

#799 In Verified-zkEVM/ArkLib;

· dtumad opened on Aug 24, 2026

Bump to Lean v4.33.1 (kernel soundness patch)

Status: Open.

#796 In Verified-zkEVM/ArkLib;

· dtumad opened on Aug 22, 2026

Adopt the Lean module system in ArkLib

Status: Open.

#795 In Verified-zkEVM/ArkLib;

· dtumad opened on Aug 22, 2026

feat(coding-theory): ListLowerWitness/ListUpperWitness constructors for GrandChallenges

Status: Open.

#789 In Verified-zkEVM/ArkLib;

· aryaethn opened on Aug 21, 2026

Enforce axiomsweep in CI (currently report-only)

Status: Open.

#764 In Verified-zkEVM/ArkLib;

· alexanderlhicks opened on Aug 16, 2026

AGM.GroupRepresentation is under-constrained: no basis/exponent length agreement, and a ZMod p exponent without an order hypothesis

Status: Open.

#707 In Verified-zkEVM/ArkLib;

· aryaethn opened on Aug 9, 2026

Sequential-composition and context-lifting layer is stubbed, making composed security theorems vacuous

Status: Open.

#676 In Verified-zkEVM/ArkLib;

· alexanderlhicks opened on Aug 2, 2026

Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan

Status: Open.

#627 In Verified-zkEVM/ArkLib;

· Abraxas1010 opened on Jul 10, 2026

ROADMAP.md is out of date (unchanged since June 2025)

Status: Open.

#608 In Verified-zkEVM/ArkLib;

· aryaethn opened on Jul 5, 2026

doc(oracle-reduction): add conceptual documentation for Basic.lean

Status: Open.

#480 In Verified-zkEVM/ArkLib;

· Sfgangloff opened on Apr 29, 2026

Definition & Security Proofs for Merkle Trees

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#4 In Verified-zkEVM/ArkLib;

· quangvdao opened on Dec 18, 2024