Smart Contract Formal Verification

Errare humanum est, but a single typo in the code can translate into millions of dollars in losses. In this respect, smart contracts are as prone to errors as any other software. In 2021 alone, $680 million of blockchain-based digital assets secured by smart contracts were lost due to code flaws. According to a recent survey, smart contract programmers often sacrifice security to deliver projects on time, expecting external auditors to make their code squeaky clean. That’s why the self-executing code of new smart contracts desperately needs formal verification. 

What is Formal Verification?

This is a maths-based technique of making sure that a system works like a clockwork within its environment. Formal verification has been used in a variety of spheres since the late 1960s. If not for this method, NASA’s Mars Rover could be a failure. 

When it comes to the blockchain ecosystem, formal verification is a life savior. Once smart contracts start to be executed, nothing can stop them. If their code contains any bugs, sooner or later someone will take advantage of them. To prevent immutable hacks, developers must prove that software is going to work as intended under any circumstances, and such proofs can only be given that it gets formally verified. A smart contract that has passed the painstaking process of formal verification behaves error-free 100% of the time. 

Why do standard testing methods fail?

It’s just too much. How does regular testing work? Once an algorithm has been written, a tester inputs a variable and checks whether it returns the correct output. However, it’s nothing else but scratching the surface. It would be physically impossible to test every single input. The devil lies in one small detail: standard testing only checks for the presence of errors, not the absence of them.

In contrast, formal verification doesn’t check each situation at a time. It finds mathematical evidence that the programming logic holds true.

Stages of the formal verification process

• Create a formal specification.

Generally, someone who has a clear idea of what the software is supposed to do needs to convey it to an engineer. The latter analyzes the requirements and makes a precise computer-checkable plan.

• Verify the model’s logic with mathematical evidence.

That’s when the magic starts, with the most trivial statements requiring proofs using multiple theorems. 

• Build the software according to the specification

As a rule, developers choose one of the functional programming languages that are close to algebra such as  Haskell, ML, or F#.

Key advantages of Formal Verification

• Easy-to-understand. The results of an audit with the help of formal verification tools resemble detailed documentation rather than a security report.
• Univocal. Unlike a manual check where human errors or uncertainty can’t be excluded,  formal verification provides us with ironclad proof that a smart contract runs or doesn’t run as intended. 
• Independent. Since math is the only universal language, it can be used to formally verify smart contracts written in any programming language, including Rholang, Solidity, Michelson, Plutus, Obsidian, etc.
• Thorough. Since it is performed automatically, formal verification gives us confidence that nothing will be missed along the way. 

Cons of Formal Verification Process

• Limited functionality

Software that has been verified using this method is limited in what it can do. 

• Complicated workflow

Even the basic algorithms need hundreds of lines of formally verified code.

• Expensive programmers

Formal verification requires knowledge of functional programming languages due to their close relation to math.

Formal Verification Tools

Smart contract programmers who lack the specific expertise essential for using formal verification techniques and/or want to make the whole process less time-consuming can make use of a few invaluable tools. These include automated theorem provers and model checkers like Metamath, Coq, Isabelle, Gloups, Lesar,  NBac, etc. 

It might sound pompous, but formal verification does appear to be a viable solution that can eliminate the chaos in the blockchain world. Performing a security audit based on formal verification techniques is the optimal way to prove that smart contracts are vulnerability-free.