Full formal verification of smart contracts using our original advanced technology

WE SECURE SMART CONTRACTS WITH FORMAL VERIFICATION

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?

high

Formal verification

Audit

Code in strongly typed language

Code review

low

Smart contract security level

Can’t find 100% of vulnerabilities, and the number of potential exploits increases with complexity of smart contracts

Find most vulnerabilities and inefficiencies

Readable audit report

Audit of smart contract: code review and testing

Formally verified smart contract works only as intended with no vulnerabilities, no matter how complex, in line with the formal specification

Verification of the code against the formal specifications

Development of readable specifications

Detailed reports that can be independently verified

Formal verification of smart contract

Andrey Lyashin

Sergey Egorov

We are an international team of highly-skilled professionals in mathematics, computer science, entrepreneurship, and economics.

Many of the team members were the winners of the national or international contests in programming and other sciences (such as physics) while others have decades of experience, scientific degrees, or previous employment in the world-class companies.

Why us?

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

FAQ

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.