halmos

halmos copied to clipboard

[Feature/#125] Enhance configuration management by using toml configuration file

1

## Change Type - [ ] Bug fix (Not Breaking-change. Solve issue.) - [x] New feature (Not Breaking-change. Add new feature.) - [ ] Breaking change (Bug fix or New...

pillip

Support properties of the form `must always emit an event when storage is updated `

3

Example here with Certora: https://github.com/Cyfrin/3-gas-bad-nft-marketplace-audit/blob/main/certora/spec/GasBadNft.spec

0xkarmacoma

wip

daejunpark

Add `cancun` support

4

`halmos` does currently not support the new EVM version `cancun` (example `MCOPY`): ```console ↩ 0x5e 0x (error: HalmosException('Unsupported opcode 0x5e')) ``` In order to formally verify properties given this new...

pcaversaccio

https://x.com/daejunpark/status/1789480206320939296 When I googled these on stream, I got no results. It would be great to place these FAQs in either: 1. In an `FAQ` section 2. A bunch of...

PatrickAlphaC

--early-exit doesn't work as expected

1

**Describe the bug** `--early-exit` is supposed to print the first counterexample found and stop halmos, but we can actually still have multiple counterexamples reported **To Reproduce** ``` // SPDX-License-Identifier: MIT...

0xkarmacoma

Improve testing of EVM correctness

1

## Problem Halmos is essentially a light EVM interpreter (without gas), and because we're in the business of looking for corner cases of EVM bytecode, it is actually mission critical...

0xkarmacoma

support multiple array lengths at once, e.g., (syntax to be decided), `halmos --array-lengths x={1,2,3}` this should be equivalent to running halmos multiple times for each length value: ``` halmos --array-lengths...

daejunpark

Create a halmos Docker image with multiple solvers preinstalled

1

Description TBD

0xkarmacoma

Support vyper jumptables

3

**Is your feature request related to a problem? Please describe.** Newer versions of vyper use jumptable-based dispatchers. We don't currently handle them very gracefully because of the mod operation. For...

0xkarmacoma