Open Issues Need Help
View All on GitHub Proof: compose the 4 block lemmas into a whole-routine spec for WithdrawalDecodeClose (blocks proven, composition missing) about 2 hours ago
enhancement help wanted area:verified-core proof
Proof: semantic specs for the 7 RlpRead routines (correspondence done, specs missing; encode side is the high-value half) about 2 hours ago
enhancement help wanted area:verified-core proof
Proof: semantic specs for the 5 RlpWalk routines (correspondence done, specs missing) about 2 hours ago
enhancement help wanted area:verified-core proof
Proof + unit-test package: bal_canonical_sort ordering and permutation (self-contained) about 2 hours ago
help wanted area:codegen proof
The program in rlp_decode_singleByte_validated can be shortened about 1 month ago
enhancement good first issue
enhancement good first issue
bug good first issue
Add a ci check against never-imported lean files 3 months ago
enhancement good first issue
Import hygiene sweep via lake exe shake 3 months ago
enhancement good first issue
refactoring: Local variables that rename lemmas 3 months ago
enhancement good first issue
enhancement good first issue
replace existing native_decide 4 months ago
bug good first issue