Runtime verification tool for Solidity smart contracts.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.

contractLarva: Runtime Verification of Solidity Smart Contracts

Gordon J. Pace <>
Joshua Ellul <>


contractLarva is a runtime verification tool for Solidity contracts. For more details about the tool check out the user manual in the docs folder.

The code is currently undocumented and not well organised. Hopefully, it will be cleaned up for the next major release.

If you would like to ask any questions, report any bugs or make any feature requests, contact us using one of the emails above.

Building the tool

To compile contractLarva, you need a recent version of GHC. The easiest option is to install the Haskell Platform which comes with all the necessary libraries included (make sure that you choose to install the full platform, not the minimal one). To compile contractLarva, then simply run the following command in the src folder:

ghc -o contractlarva Main.hs

Tool usage:

contractlarva <specification.dae> <input.sol> <output.sol>


This project is licensed under the terms of the Apache 2.0 license.

FAQ and Common Problems

When compiling the code I get the error: Could not find module ‘Text.Parsec’.

Make sure you have installed parsec. Also, see this stackoverflow thread (

cabal install parsec