Scivik

Scivik is an automated toolchain that formally verifies the functional correctness of Yul, the intermediate representation of Ethereum smart contracts.