Where reliability becomes absolute
Full formal verification of third-party Free TON smart contracts using the original advanced technology.
Almost any software has bugs. Sometimes they are innocent but for mission critical products they may lead to multimillion losses​. And for smart contracts the software bug are especially dangerous.
Formal verification provides a unique opportunity to reach an absolute reliability and safety of smart contracts basing on strict mathematical proving (in the same way as proving of theorems).
Original advanced
technology including —
Specification development for the smart contract functions and methods
Proving of high-level scenarios
Detailed report that can be independently audited
Formal verifying the code against the developed specification
Proving that compiled TVM code does the same as the original code in high-level language
So you guarantee absence of bugs?

Not exactly. Using high-level scenarios we guarantee no possibility of some serious malfunction such as spending or acquiring more than planned, magic appearance or vanishing of tokens, smart contract stalling etc.

Accordance of the internal functions and methods to the developed specification. In case the specification is not full or boggy some minor bugs still possible while the prevention of the serious bugs is described at the previous bullet.

How can we be sure you indeed proved what declared?

We provide the customer with all the sources as well as with the detailed report that can be verified either by the customer themself or by the independent auditor. We are the supplier for the leading player — TON Labs and in the nearest future we plan to get the acknowledge from the leading scholars in the industry.

What languages do you support?

All standard languages supported by TON Labs compilers with some restrictions. The preferable language is Solidity.

Any code of the smart contract can be verified?

Some restrictions are in place (they are not critical but will dramatically increase cost and time):

  • No recursions
  • No cycles with unclear exit conditions
  • No intensive usage of pointer arithmetic (for C/C++)
  • No poor-designed code (side effects, long functions etc.)
  • No concurrency
What is the expected duration of the formal verification process?

It depends on the smart contract but 1-2 months is a good initial estimation.

What is the expected price of the verification?

It highly depends on your contract. Inquire us for the details.

May I become your partner (as a franchisee or in some another way)?

At the moment, no, but in mid-term we plan a special program dedicated to involvement of independent verifiers into the ecosystem.

Inquire us for the details