SMTChecker and Formal Verification

The Solidity compiler has a built-in formal verification module called the SMTChecker. This module can be used to automatically prove properties of smart contracts.

💡 NeoVM Difference

The standard solc SMTChecker module operates specifically on the behavioral constraints of the EVM (like 256-bit arithmetic boundaries and sequential storage slots).

Neo DevPack for Solidity does not currently include the SMTChecker.

Because NeoVM uses arbitrary-precision integers (BigInteger) internally, Neo DevPack for Solidity implements fixed-width overflow behavior with compiler/runtime guards rather than native EVM word overflow. Standard EVM SMTChecker results are therefore not a direct proof for generated NeoVM artifacts; use them as source-level hints and validate arithmetic behavior with Neo DevPack for Solidity tests.

Verification on Neo

Currently, verifying Neo DevPack for Solidity contracts requires external auditing tools or testing frameworks. We recommend utilizing the tooling/ packages in this repository (like @neo-devpack-solidity/hardhat-solc-neo) to run extensive unit and integration tests against local Neo-Express nodes.

Future iterations of the compiler may introduce Neo-specific constraint checkers for static analysis, specifically regarding:

1. Manifest Permission Wildcards: Validating that all cross-contract calls are strictly bounded.
2. Witness Checks: Statically analyzing functions to ensure Runtime.checkWitness is executed prior to any state-mutating operations.