SMTChecker: Validating solidity code

25 Apr 2024

SMTChecker is a powerful built-in solc feature. SMTChecker enables formal verification of solidity code directly using the solidity contracts. While this feature is unused and underappreciate today, I hope this post may help change that.

Installation

There are no step-by-step installation instructions in the solidity docs for SMTChecker, which would be nice to change in the future. I found two easy ways to use SMTChecker:

1. Use remix, which has SMTChecker built-in to the WebAssembly binary. The line pragma experimental SMTChecker; must be added in remix to activate SMTChecker.
2. Install a dynamic (not static) z3 library on a *nix system (you can use docker or a VM), which the *nix solc binary on the releases page will automatically use. To install the dynamic z3 library on Ubuntu, you can use sudo apt install libz3-4 libz3-dev, which should add a libz3.so file to one of your default library paths such as /usr/lib.

If SMTChecker cannot find z3 on your system, it should return a warning message such as Warning: z3 was selected as a Horn solver for CHC analysis but libz3.so.4.8 was not found. .

Shortcomings

Before moving further, be aware that SMTChecker does not support assembly code. SMTChecker currently ignores assembly code. If you want a comparison of some other similar tools, this medium post and this stack exchange answer may be useful.

Using SMTChecker

The are many options and arguments that can be used to customize how SMTChecker runs. These options are clearly labeled in the output of solc --help. Most options have sensible defaults that I leave as they are, but the options I use most often are:

1. --model-checker-engine: without this option, the SMTChecker will not run and will not catch any assertion violations. This option can be set to all, bmc, or chc. I normally use chc or all.
2. --model-checker-timeout: setting this option to zero will remove resource restrictions for the SMTChecker. If this option is not used, the SMTChecker may stop running before it finishes, resulting in incomplete outputs. I normally set this to zero to remove any limits.
3. --model-checker-show-unproved: The SMTChecker will sometimes output a message suggesting to add this option because it did not finish proving all invariants. I sometimes add this option, but because the SMTChecker generally suggestions when adding it is useful, I don’t always add this option.

Unusual error

I encountered an unusual (and dumb) error with SMTChecker that I will describe in case it saves someone some troubleshooting. I thought SMTChecker was not detecting z3 because the output from running SMTChecker had many blank lines with only a few words like “Warning” and one line of code showing in the output. The issue was that the output from SMTChecker was actually correct, but the terminal font colors I was using rendered most of the output invisible. It was only by copying the output (with “blank” lines included) into an empty text file that I detected the issue. Lesson learned, blank lines aren’t always blank.

Concluding Remarks