Formal Verification Service

Formal verification is the process of mathematically proving that a hardware or software system meets the required specifications.

Nowadays programmers write unit tests to make sure the program conforms to certain characteristics. They test the program with as many inputs as possible, each time checking that the input matches the specified specifications. For example, to check if a program sorts a list of numbers in ascending order correctly, it would test with the input [2, 3, 1]. The result should be: [1, 2, 3], otherwise the program will be considered invalid.

However, the unit testing approach may not take into account all possible inputs (or edge cases), which can cause the program to fail. The solution to this problem is formal verification. Formal verification involves writing mathematical definitions of the program. Using the same example as above, one could write the definition: «For each element j in the list, make sure element j ≤ j+1». This is a huge improvement over unit tests, as program correctness is mathematically universal.

The main application of smart contracts is related to the implementation of distributed registries, the blockchain, the basis of which is the absence of an intermediary between the parties signing a smart contract. Nevertheless, it is very likely that with the development of digital technologies, smart contracts will be able to become the main guarantor of the execution in the broadest sense of the legal conditions for the execution of an agreement concluded between two or more parties.

Smart contracts have a number of disadvantages:

• Smart contracts are based on program code, any error in the code leads to incorrect execution of the contract, this imposes high requirements on the accuracy of the contract description, as well as increased responsibility on the developer of the program code.
• When creating a complex smart contract that must take into account the behavior of several parameters of the conditions for the execution of a contract at once, the contract developer needs to control the behavior of several conditions of a complex multicomponent contract system at once. This makes the process of creating a contract a difficult task that not all developers are ready to take on.
• The impossibility of reviewing the result of the execution of a smart contract and making changes after accepting the terms of the agreement between the parties. At the moment, there is a discussion of the introduction of the possibility of the existence of a smart contract by a third independent party, with a confirmed legal status and the right to make changes to the program code of the smart contract, which would allow not to recreate a new contract, but to correct an existing one, if in the process of interaction of the parties to the contract came to the understanding that the conditions for the execution of a smart contract need to be reviewed.
• Uncertainty of the legal status of the smart contract. At the moment, the smart contract does not have a legal status, primarily due to the impossibility of revising the conditions for its execution.

These shortcomings require us to think about the introduction of additional verification/testing of the smart contract program code to increase the reliability and correctness of the conditions for its execution.

One way to solve this problem is to use formal verification of smart contracts. Formal verification is a formal modeling of the system, which allows you to see and verify the correct functioning of the simulated system and highlight its weaknesses. Also, formal verification can serve as a bridge for understanding between the developer of the contract and its customer.

Often, customers want to be sure that a fixed smart contract performs exactly the actions and according to the conditions agreed upon by the parties to the contract. But how can you be sure of this if the parties to the contract do not know programming languages?

One of the solutions is to build automata and diagrams based on the formal smart contract model. Diagrams and graphs regarding the program code have a lower threshold for perception, they are easier to read and clearer, and it quickly becomes clear what exactly and how the smart contract does.

Smart contracts are programs containing a certain amount of money. Therefore, it is very important that they are error-free and accurate. Unit testing is not enough to cover all the edge cases and bugs that may occur.

Complex financial contracts involve steps and processes that involve the trust of the parties involved, as well as the parties concerned with the reliability of the system on which the contract is built. An improperly drafted contract can destroy the credibility of the system. In the worst cases, unintentional software glitches can lead to loss of money, as happened with Ethereum.

The stage of formal verification of smart contracts can be compared with the presence of an intermediary institution that checks the correctness of the logic and validates the correctness of the stated contract conditions. The use of formal verification and formal modeling can greatly reduce the time costs of developing contracts by checking their correctness at the early stages of contract development.