Repository navigation

All pull requests

Labels (12)Milestones (1)New pull request

Open

(23)

Closed

(391)

perf: run gc at safe points and share completed call history
#606DicksonWu654 opened Nov 6, 2026
perf: reuse a thread-local context for path serialization
#605DicksonWu654 opened Nov 6, 2026
fix: correct EVM opcode semantics for NOT, ADDMOD/MULMOD, RETURNDATACOPY, MLOAD
#604feafel opened Nov 4, 2026
feat(sevm): support CLZ opcode (0x1e, EIP-7939)
#603ninglinLiu opened Oct 28, 20262 tasks done
fix(bitvec): return 0 for ADDMOD/MULMOD when modulus is zero
#602ninglinLiu opened Oct 28, 20261 task done
fix(sevm): bitwise NOT after comparisons; keep JUMPI fallthrough
#601ninglinLiu opened Oct 28, 20261 task done
fix(sevm): expand memory on MLOAD; bounds-check zero-size RETURNDATACOPY
#600ninglinLiu opened Oct 28, 20261 task done
fix: parse alternative Foundry artifact paths and disambiguate libraries
#599mrchandu1462-ux opened Oct 24, 2026
fix(bitvec): return 0 for concrete ADDMOD/MULMOD with a zero modulus
#598mayuriphad opened Oct 21, 2026
2
fix: use bit size for sha256/ripemd160/modexp precompile input sorts
#592joshdrv opened Oct 3, 2026
fix: model SHA-256 precompile input widths in bits
#591DicksonWu654 opened Sep 1, 2026
Fix msg.value balance accounting in invariant tests
#590DicksonWu654 opened Sep 1, 2026
Fix vm.sign malleable recovery value
#589DicksonWu654 opened Sep 1, 2026
Fix concrete zero-modulus ADDMOD and MULMOD
#588DicksonWu654 opened Sep 1, 2026
Use modular exponentiation for concrete EXP
#587DicksonWu654 opened Sep 1, 2026
Fix syntax for dynamic array initialization in Solidity
#58475748 opened Jun 11, 2026
Support of OPCODE BLOBBASEFEE , BLOBHASH and CLZ
#583HugoDowsers opened May 18, 2026
3
fixed Morpho Halmos test link
#581inmarelibero opened Jan 19, 2026
fix: symbolic storage variables in counterexample + add path id to co…
#5780kn0t opened Sep 12, 2025
5
Enhance div_xy_y to support signed and unsigned division simplification
#576sidarth16 opened Sep 10, 2025
13
Implement global PopenExecutor with tagging for improved process control and probe isolation
#5410xkarmacoma with CopilotAI opened Jun 11, 2025
31
fix: we do support empty bytes now
#4620xkarmacoma opened Feb 16, 2025Contributor
7
fix modexp type mismatch
#4140xkarmacoma opened Nov 14, 2024Contributor
1

Navigation Menu

Repository navigation

All pull requests

perf: run gc at safe points and share completed call history

perf: reuse a thread-local context for path serialization

fix: correct EVM opcode semantics for NOT, ADDMOD/MULMOD, RETURNDATACOPY, MLOAD

feat(sevm): support CLZ opcode (0x1e, EIP-7939)

fix(bitvec): return 0 for ADDMOD/MULMOD when modulus is zero

fix(sevm): bitwise NOT after comparisons; keep JUMPI fallthrough

fix(sevm): expand memory on MLOAD; bounds-check zero-size RETURNDATACOPY

fix: parse alternative Foundry artifact paths and disambiguate libraries

fix(bitvec): return 0 for concrete ADDMOD/MULMOD with a zero modulus

fix: use bit size for sha256/ripemd160/modexp precompile input sorts

fix: model SHA-256 precompile input widths in bits

Fix msg.value balance accounting in invariant tests

Fix vm.sign malleable recovery value

Fix concrete zero-modulus ADDMOD and MULMOD

Use modular exponentiation for concrete EXP

Fix syntax for dynamic array initialization in Solidity

Support of OPCODE BLOBBASEFEE , BLOBHASH and CLZ

fixed Morpho Halmos test link

fix: symbolic storage variables in counterexample + add path id to co…

Enhance `div_xy_y` to support signed and unsigned division simplification

Implement global PopenExecutor with tagging for improved process control and probe isolation

fix: we do support empty bytes now

fix modexp type mismatch

Pull requests