Full formal verification of smart contracts using our original advanced technology
Off-chain monitoring using AI-based tracking of smart contract activity
Smart contract monitoring
Using our verified libraries end methods
Formal verification
Using Ursus — Coq embedded language
Development support
We provide complex solution to the critical security problem
Our workflow
The key advantage of using our service is the dramatic increase in security against the risks of stealing, freezing and improper distribution of critical assets compared to other existing solutions
Why formal verification?
Formal verification
Code in strongly typed language
Code review
Smart contract security level
Formal verification of smart contract
Detailed reports that can be independently verified
Development of readable specifications
Verification of the code against the formal specifications - proving that smart contract is 100% correct against formulated specification
Audit of smart contract: code review and testing
Readable audit report
Find most vulnerabilities and inefficiencies
Protected systems
Ask us for the details and we’ll make it worth your time.
Interested in unprecedented security for your smart contracts?
If you didn’t find the answer for your question feel free to contact us via email
So you guarantee the 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 the detailed report that can be verified either by the customer himself 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.
How can I become your partner?
Inquire us for the details.
Made on