We’ve previously discussed formal software verification as related to crypto programming.
Today we’d like to discuss an intermediary concept called semi-formal cryptocurrency development.
In formal verification, every single possible logical state of a computer program must be mathematically proven.
This kind of proof can consume tens, even hundreds, of pages of mathematical notation for very simple things.
For example: Formal verification of a sorting procedure which organizes whole numbers from smallest to largest may require a mathematical proof which is tens of times larger than the sorting program itself.
Semi-formal verification seeks to avoid this explosion in formal proof size by combining intense testing procedures with formal verification of critical sections of the software code.
Many approaches exist to semi-formal verification, since it’s not a strict discipline.
Developers from many fields take different approaches at semi-formal software verification.
In a cryptocurrency implementation, the user interface, web components, styles and other auxiliary code aren’t critical and may skip formal verification. Well designed testing procedures will catch most errors in these kinds of applications.
But the routines which save and retrieve data from the blockchain may have critical sections be formally verified.
For example, it is impossible to test all possible cryptocurrency input addresses, since the search space of 256 bit and larger numbers is astronomic.
But it is possible to prove facts about large numbers without testing them all. Using mathematical induction, for example, it is possible to prove that a certain routine is correct given whole numbers as input – no matter how large they are.
This, combined with exhaustive search for other common errors, yields good quality software without having to formally verify every single aspect of it.
Using formal verification together with brute force testing is an example of a semi-formal method.
CertiK seems to be gaining popularity for cryptocurrency formal verification.
It uses semi-formal methods including searching for common errors in smart contracts, known bug patterns and other “code smells”.
Several large cryptocurrency projects use this Binance-funded framework.
Cardano was built from the start with formal verification in mind.
The goal is to allow Cardano smart contracts to be formally verified both for legal compliance and for business logic correctness.
Cardano uses the Haskell programming language which is tightly linked to the mathematical concepts required in formal verification.
We hope this short intro to semi-formal verification has helped get a better understanding of this testing methodology and how it relates to cryptocurrency development. In the future you are likely to see many crypto projects employ semi-formal methods.
If regulations catch up with the cryptocurrency field, formal methods may even become legally mandatory for critical and safety-intense applications in the future.
Integrating semi-formal and formal software specification techniques
Best of both worlds [formal and semi-formal software engineering]
Use of Semi-Formal and Formal Methods in Requirement Engineering of ILMS