Make most critical systems verifiably credible
We provide cybersecurity solutions that are based on a formal verification technology stack, empowered by in-depth scientific research.
Supported systems

SERVICE CASES

Formal specification for TON Virtual Machine Assembler
Everscale
https://github.com/everx-labs/ever-assembler
Created formal specification for TVM Assembler. While it’s not a smart contract, but rather part of the node, its intention is to convert a stream of primitives with parameters into a cell that can be loaded into a TVM machine.
Deductive formal verification - Multisig
smart contract
Everscale
https://docs.google.com/presentation/d/1jn7vTD38atskaKf9oNM5pu0UmrG8aeJSwhoEbafTEiE/edit?usp=drive_link

Solidity smart contract - an Everscale cryptocurrency wallet that can require multiple signatures to make any payment. The list of eligible “custodians” as well as a number of signatures required can be altered as a separate action or by upgrading the full contract code. Both actions are allowed by the approval of the strong majority of custodians.
We designed business-level specification, described user scenarios and performed formal full deductive formal verification, uncovering several critical exploits overlooked by a series of common audits.
Result: advised on the rework of smart contract and completed formal verification, so now the system can be considered 100% predictable.
Deductive formal verification - Vesting smart contract system
Everscale
Vesting system distributes a predefined amount of tokens to the recipient, splitting the amount into a set of monthly uniform tranches.
We designed a formal specification and proved all the properties of the system of smart contracts, so it is considered as 100% predictable, successfully deployed and no bugs or exploits were encountered since.

Development of stable token system
Everscale
https://github.com/Pruvendo/not_oracle
System of two solidity smart contracts: validator and elector and a web application. Successfully developed and deployed on blockchain
Development of auction smart contract
Free TON
https://github.com/Pruvendo/freeton-auctions
Development of Solidity smart contract. This versatile system can handle a wide variety of auction types and also implement other scenarios like a cascaded auction. All the auctions are thoroughly tested and accompanied by the depots that allow to deal with auctions in the interactive mode. Implemented types of auctions: English, English first price, English reverse, First price reverse, Dutch straight, Dutch reverse
Audit of solidity smart contract
Dune Network merge with TON
https://gitlab.com/dune-network/ton-merge/-/tree/993377f5df07b4b42811ec995874bc9b986cea49/contracts/free-ton
The Dune to Free TON merger smart contract system manages the configuration of the merge (in particular, the list of users (relays / oracles) that can confirm transactions that replicate Dune orders on the Free TON side. It also deploys UserSwap contracts upon eligible relays’ requests, accepts and sends tokens to UserSwaps. In this audit we uncovered several issues and advised on improvements and corrections.

Formal verification of the Elector smart contract
Everscale
The Elector is a system smart contract that is intended to periodically elect a set of validators that check the correctness of transactions using the PoS paradigm. Each candidate places some deposit and the candidates with higher deposits are elected as validators being awarded with some fee for each transaction validated while any malicious validators should be slashed with withdrawal of their deposits in honor of the community. During the verification process, we uncovered several critical issues, then advised on improvements.
Development of formal specification and deductive verification of DePool
Free TON
https://github.com/Pruvendo/depool_contract
Tokenomics audit
FLEX DEX
Formal specification design
FLEX DEX
https://flexdex.fi/
Audit of smart contract
NFT marketplace GRANDBAZAAR
https://grandbazar.io/

TECHNOLOGY CASES

Automation of formal verification tested with benchmarks project
Ethereum foundation
https://github.com/eth-sc-comp/benchmarks/
Performed trials of Ethereum Foundation's Benchmarks Project: optimized the process of deductive formal verification with Ursus meta language. Integrated our process into ETH benchmarks pipeline, including pre-generation and launching tools on generation artifacts, making it possible to measure time of execution and to compare our approach with other solutions. Since that moment the manual efforts we spent for formal proof can be reduced to one line proof in many cases.
Deductive Formal verification showcase
MultiversX
https://github.com/multiversx/mx-sdk-rs/blob/master/contracts/examples/crowdfunding-esdt/src/crowdfunding_esdt.rs
During the MultiversX hackathon in October 2023 we’ve successfully added support for the Rust language to Ursus online translator, providing capabilities of our deductive formal verification toolkit to the Rust developers community. And demonstrated results, automatically translated MVX Adder smart contract from Rust into Ursus.

In this showcase of our formal verification approach we proved properties   MVX Crowdfunding smart contract.

1. Translated smart contract into Ursus. (screen 1)
2. Formulated smart contract's properties in Coq (screen 2)
3. Proved them (screen 3) - we’re on the way to improving proof automation for Rust.

Result: this is a complex Rust smart contract which passed deductive formal verification. So now we are open to cooperation in formal verification and cybersecurity with teams building with Rust and MultiversX in particular.
Rust support for Ursus Online translator
https://www.youtube.com/watch?v=STwJCoqNeCc&ab_channel=Pruvendo
We've added Rust support to our translation tool to provide our security and development services to MultiversX ecosystem.
Implemented TVM Solidity syntax highlighting for VS Code
Everscale
https://github.com/tonlabs/ever-assembler
PRODUCTS
Automated formal proof in several clicks
For Rust and Solidity smart contracts
Create math model of smart contract in minutes using buttons in Ursus Online constructor
FAQ
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.