Firefly helps Ethereum smart contract developers by illuminating holes in their contract's test-set, guiding them towards higher test coverage and thus higher code quality assurance. A definite must for any smart contract developer planning to store and manipulate user funds.
Running Firefly on your contracts reduces the work needed for formal verification, which means saved time. Consider setting up Firefly on your repository before contacting us for more in depth formal verification services.
Below is our tentative release timeline:
December 2019 - Run your tests using KEVM directly on CI. Benefits include increased performance and higher assurance in the correctness of the EVM implementation.
January 2020 - Report test coverage of your EVM bytecode on CI to track holes in your test-set.
April 2020 - Runtime verify temporal properties of your contract. Leverage your tests by additionally checking temporal properties of their executions.
July 2020 - Automated contract verification for preset contract types (ERC20, ERC777, etc...).
August 2020 - Assertion violation checker. Double-check that your Solidity assertions will actually hold in all cases.
October 2020 - Bounded model checker. Exhaustive state-space exploration of your contract's executions using symbolic execution to look for potential bugs missed by your tests.
December 2020 - Automated test-case generation for any bugs found by the other tools. Incorporate the new tests into your test-set to catch the same bugs earlier next time.
Interested in the future of Firefly? Sign up for updates below.