Blog
Docs
Make Your 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

We support systems with Solidity and Rust smart contracts
EVM, TVM and MultiversX VM

SERVICE CASES

We provide secure Development of smart contracts, Audit, Formal specification and Deductive formal verification to ensure credibility and security of critical systems for either simple or complex multi-contract asynchronous systems.
Formal specification for TON Virtual Machine Assembler
Everscale
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
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
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
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
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.

Development of formal specification and deductive verification of DePool
Free TON
Formal specification design
FLEX DEX
Audit of smart contract
NFT marketplace GRANDBAZAAR

TECHNOLOGY CASES

We research formal methods and other applied mathematics to develop Ursus Tech Stack and
Formal Specification tools
Automation of formal verification tested with benchmarks project
Ethereum foundation
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.
Implemented TVM Solidity syntax highlighting for VS Code
Everscale

TOOLS
Automated formal proof in several clicks
For Rust and Solidity smart contracts
Create math model of smart contract in minutes using
Ursus Online constructor
  • Debug with graphical display of transactions
  • Supports: Gosh, Everscale, Venom
ROADMAP OF PRUVENDO
May 2019
The inception of the Ursus idea as a tool of verifying smart contracts based on the Coq DSL
Aug 2019
Initiated development of the base lib for contract verification.
Nov 2019
Development of monadic representation of contracts, first contract ongoing verification (Multisig in TON)
May 2020
Created TVM assembler modeling in Coq
Nov 2020
Developed Ursus v1
Jun 2022
Developed exec generator
Feb 2022
Started randomized testing development
Nov 2022
Seed investment round, private equity
Dec 2022
Partnership with Gosh.sh
Dec 2023
Ursus v32 - last major version
Sep 2023
Rust support added
Oct 2023
Multiversx collaboration
Jan 2024

ETH benchmarks completed.

Formalization and verification of social choice theory (Voting).
Mar 2024
Significant optimization of exec generator (up to 10,000,000 times faster)
Apr 2024
Formal verification of Voting protocols with Gosh and Jocelyn DAO presentation
May 2024 plans
Ursus online beta.
Support for TRON smart contracts.
Jun 2024 plans
FunC (TON smart contracts language) early support.
Support for semiautomated verification of loops in Ursus Online.
July 2024 plans
Commencement of AI proof goals research
Aug 2024 plans
Open beta of Graphical collaborative Formal Specification tool.
Ursus-scrypt release.
Dec 2024 plans
Implementation of AI verification goal classifier.
Second major version for specification language.
If you have any questions, join our Discord.
We're always open for discussion.
FAQ
Where is Pruvendo legally incorporated?
Pruvendo-FZCO is incorporated in Dubai, UAE.
Do you focused on Web3 security only?
We are a technology company and our major focus is on Formal Methods R&D. We believe it's possible to make formal verification tools and services usable for the wider community of software developers (as for now FV is popular mostly in SoC design).

Smart contracts are relatively small programs and in the current state of formal verification of software technology stack it is the best test site for making R&D economically viable.
So you create tools for formal verification?
We develop a toolkit for software development and verification. It consists of Formal specification tools, Formal verification tools and QA tools.
Does Pruvendo toolkit suitable for smart contracts only?
For now, we support only Solidity and Rust languages. Our formal verification approach doesn't rely on VM, so we can potentially support most strongly typed languages without direct memory access in the future. So we hope to create a robust toolkit suitable for deductive formal verification of most software.
What are the main obstacles for wide spread of formal verification?
Agile (iterative direct to market prototyping) methodologies of software development. In the current state of technology, formal verification is a great approach only if the product or system has strict specification. Otherwise, it's not viable, especially in a continuous development approach.

So our long-term goal is to make formal verification tools helpful even in cases of continuous product changes.
Which chains do you support for development of smart contracts?
We're not chain-binded and can quickly support any blockchain with Solidity or Rust smart contracts (other languages will require us to add support to our Ursus Online translator first, so it will take + 1 or two months to prepare for the project development/verification).
How about web2 security?
Members of our team have in-depth expertise in traditional cybersecurity, we're open for a discussion in our Discord