Formal Verification

Formal verification refers to the process of ensuring that a system, such as a set of smart contracts, is mathematically correct based on a list of established requirements. Instead of using explicit states, formal verification should work with symbolic input variables (layer of abstraction). As a result, it is typically through applied mathematical modeling that these tests can be conducted. An Ethereum contract that passes the verification process may be included in one of the following categories: 'functionally correct', 'correct by design', or 'correct by construction'.