Verified-zkEVM

Verified-zkEVM/evm-asm

13 good first / help-wanted issues · Lean · last activity Jul 28, 2026

51 stars 14 forks 51 watchers Lean MIT License
View on GitHub
13 Open Issues Need Help Last updated: Jul 28, 2026

Open Issues Need Help

View All on GitHub
parallel lane: the 251 loop-free-with-calls routines — callee-row composition contracts, demand-ranked worklist, independently claimable rows about 1 month ago
help wanted area:verified-core proof
Verified-zkEVM/evm-asm
51

Lean
Proof: semantic specs for the RLP encode side — rlp_encode_uint_be and rlp_encode_bytes absent, rlp_item_size/rlp_encode_list_prefix long forms uncovered (2 of 7 already done) about 2 months ago
enhancement help wanted area:verified-core proof
Verified-zkEVM/evm-asm
51

Lean
Proof + unit-test package: bal_canonical_sort ordering and permutation (self-contained) 2 months ago
help wanted area:codegen proof
Verified-zkEVM/evm-asm
51

Lean
Proof: semantic specs for the 5 RlpWalk routines (correspondence done, specs missing) 3 months ago
enhancement help wanted area:verified-core proof
Verified-zkEVM/evm-asm
51

Lean
Proof: compose the 4 block lemmas into a whole-routine spec for WithdrawalDecodeClose (blocks proven, composition missing) 3 months ago
enhancement help wanted area:verified-core proof
Verified-zkEVM/evm-asm
51

Lean
The program in rlp_decode_singleByte_validated can be shortened 4 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
CI: verify RLP spec against execution-specs (tests or proofs) 5 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
Standardize variable naming convention (camelCase vs snake_case) 6 months ago
bug good first issue
Verified-zkEVM/evm-asm
51

Lean
Add a ci check against never-imported lean files 6 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
Import hygiene sweep via lake exe shake 6 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
refactoring: Local variables that rename lemmas 6 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
DivMod: Split monolithic LimbSpec.lean and LoopDefs.lean by phase 6 months ago
enhancement good first issue
Verified-zkEVM/evm-asm
51

Lean
replace existing native_decide 6 months ago
bug good first issue
Verified-zkEVM/evm-asm
51

Lean