Verified-zkEVM

Verified-zkEVM/evm-asm

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

Open Issues Need Help

View All on GitHub
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) 4 days 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) 7 days ago
help wanted area:codegen proof
Verified-zkEVM/evm-asm
51

Lean
Proof: semantic specs for the 5 RlpWalk routines (correspondence done, specs missing) 9 days 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) 9 days ago
enhancement help wanted area:verified-core proof
Verified-zkEVM/evm-asm
51

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

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

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

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

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

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

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

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

Lean