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.

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.

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.

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.