FORVES 2.0: FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations
This project is developed using Coq 8.16.1 and requires the package coq-bbv version 1.4. It can be compiled with the following commands:
$ coq_makefile -f _CoqProject -o Makefile
$ make
The code is licensed under the GNU General Public License 3.0, also included in our repository in the COPYING file.