Formal verification in Free TON: by Sergey Egorov

Formal verification in Free TON: by Sergey Egorov

In April, Sergey Egorov, сo-founder of Pruvendo and one of the Formal Methods Sub-Governance founders, told Free TON House about formal verification.

Now we asked Sergey to share news about the formal verification process in Free TON and to summarize the intermediate results. 

Starting from scratch: verification stages

The formal verification process will consist of four or five stages: zero, first, second, third, and fourth (optional). 

The initial stage is divided into two phases for a reason. Phase zero is a manual source code audit based on our experience. First of all, this is done in order to ensure the code quality, and secondly, to send it out for beta use, if necessary. 

Formal verification is a long process, and business often requires a much quicker response. Therefore, we provide business with an option: either to move quickly but with a lower security level, or for a longer time but with a higher security level. 

What’s been done so far?

Three teams are actively working on formal verification: 

  • Pruvendo
  • Moscow Infotech team
  • Paris-based OCamlPro

Completely verified:

Audits of smart contracts were carried out:

  • SMV 
  • Flex (DEX Implementation from TON Labs)
  • DuneSwap (Dune Community Membership Compensation Solution) 

DEX implementation from Radiance is on its way.

What’s next?

Right now we are mostly involved in the implementation of phase zero and phase one. We are gradually approaching the second stage — verification at the so-called functional level (basically, the equator of the entire process). In the coming days, we plan to start this kind of work for the Flex contract, and then for SMV.

Plans for the relatively near future include a large and extensive work on BFTG.

In addition to the contracts’ verification, we are ready to start Free TON virtual machine verification. The first module to be verified will most likely be Executor. 

Also, when the number of verified smart contracts increases, we plan to come up with a solution that will distinguish them from the rest: a signature, a catalog or something similar. 

Are there any challenges?

Many details have to be checked with the developers — there is specific information that is not covered by the documentation. 

The quality of smart contracts leave much to be desired.  Only contracts from TON Labs can be singled out, the others still lack specifications and examples. But it’s moving along.

Find out more about the Everscale
Subscribe to our social networks and stay up to date with the latest news
SUBSCRIBE ON SOCIAL
Free TON House
Origin