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.

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.

A formal verification (as an advanced form of an audit that dramatically decreases chance for important bugs) for smart contracts of Molecula project, as well as a traditional audit for web application of Molecula project

a formal verification (as an advanced form of an audit that dramatically
decreases chance for important bugs, in a light form known as quickchicks) for Wallet smart contracts of Hipo project (https://github.com/HipoFinance/ )

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.

System of two solidity smart contracts: validator and elector and a web application. Successfully developed and deployed on blockchain

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

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.

Detailed functional specification of the FLEX - decentralized stock exchange with Depth of Market. The created specification is supposed to be turned into a formal specification and later used for the formal verification of the product.

Perform an audit of the central smart contracts (DEXClient, DEXConnector, DEXPair, DEXRoot RootTokenContract, TONTokenWallet ) in the DEX solution developed by Radiance.

Report provides the findings about the current version of True NFT smart contract jointly developed by RSquad and TonLabs.

An audit of the Solidity smart contracts developed as a part of a decentralized token exchange (DEX).

Development of detailed functional specification of the Everscalend - decentralized lending system.

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.

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.

We've added Rust support to our translation tool to provide our security and development services to MultiversX ecosystem.

Full-stack ecosystem for Everscale smart-contract verification
● Based on Coq custom grammar support
● Supports Solidity and C++
● Can be used as an independent language for smart-contract
development
● Supports fast proofs with QuickChick
● Full fledged deductive verification in Coq

There is a task of verifying smart contracts for solidity.
For this goal, Coq is used, in which smart contracts are described in a special Ursus language, therefore, in order to verify a specific smart contract, it is necessary to describe it in Ursus. This process requires a lot of manual labor and special skills, and there is a human error factor. For this purpose, a translation system is being created and developed.