Liquidswap passes formal verification by MoveBit – here’s what it means

Liquidswap DEX has successfully passed formal verification by the leading security firm MoveBit. But what is formal verification in blockchain and what makes it more powerful than a regular smart contract audit?

TL;DR

• Formal verification is a powerful way to check a smart contract (or any other software system) for vulnerabilities. Unlike regular audits, it is based on mathematical proofs.
• A mathematical model (formal specification) is created, describing how the contract should behave. The code of the contract is also translated into mathematical statements. Then, using a special tool called a prover, one verifies that actual contract behavior matches the specifications for any possible values of the variables.
• Formal verification can prove that a contract will work as expected under any circumstances - something that manual audit and testing can’t do (as it would be impossible to test a contract for all the possible variable values). It can also detect vulnerabilities that normal testing can miss.
• Move and Aptos are uniquely adapted to formal verification, because the Aptos framework already includes an automated tool called Move Prover, as well as Move Specification Language (MSL) - an easy way to turn code in Move into verification-ready statements.
• Liquidswap has successfully passed formal verification by MoveBit. Six contracts related to our concentrated liquidity AMM were verified, and only one real issue was found, which was fixed straight away.
• Formal verification is an important step for Pontem, as it is a rigorous mathematical proof that our smart contracts don’t contain vulnerabilities. Pontem is one of the few projects on Aptos and in the DeFi space overall to offer such a level of security assurance to users.

What is formal verification?

Formal verification is a mathematics-based method of checking if a system works as intended. This system can be a smart contract, a software program, an AI model, a piece of computer hardware, etc.  

To perform a formal verification of a smart contract, you need to complete these steps:

1) Define the correct (desired) behavior and properties of the system. For example, when a user initiates a token swap on a DEX, the contract must check that the user has enough tokens in the wallet to complete the swap.

2) Create a mathematical model (consisting of functions) that describes the correct behavior of the smart contract. It’s a more formal and abstract representation of the contract than its source code. For each desired property and instance of behavior, you’ll have a separate mathematical statement; together, these statements are called a formal specification.

A mathematical statement that describes the correct behavior or intended property of a contract is also called an invariant. This means that under any circumstances, whatever the input, the contract should do exactly what you want it to do – without variants.

3) Create a mathematical model for the actual smart contract.

4) Run a special tool (called a prover or a model checker) to verify that the actual contract’s behavior corresponds to the formal specification.

5) If the process can’t be completed successfully, refine the mathematical models (for example, split  a step into smaller contract actions and create more detailed statements for each).

Major blockchain projects that have had some of their contracts formally verified include Uniswap,  SushiSwap, and MakerDAO.

Provers vs. model checkers

Formal verification tools come in two types – provers and model checkers:

• A model checker goes through all possible states of the contract looking for those that would violate the rules defined in the formal specification.
• A prover proves mathematical theorems to show that the contract will behave exactly as defined by the formal specifications – in other words, that the contract will always exhibit the desired behavior, whatever the inputs or circumstances. Unlike checkers, most provers aren’t fully automated and require a human to

You can find more info on checkers and provers here.

Formal verification vs. manual audit

Formal verification, traditional smart contract audit, and testing complement each other – it’s always better to perform all three. Formal verification provides the following advantages:

• can detect vulnerabilities that manual auditors and testers miss;
• can verify that a contract will produce correct behavior for any possible input data – while actually testing it on an infinite number of input values would be impossible;
• can find errors before a contract is deployed, reducing the costs to fix them and accelerating the process of development;
• can prove that vulnerabilities are absent, whereas a manual audit can only reveal them if they are present.

At the same time, formal verification has drawbacks compared to manual audit and testing. It is expensive and requires highly skilled professionals. Transforming contract code into mathematical statements is a very complex task, and so is creating a formal specification. Moreover, if this isn’t done correctly the first time, verifiers need to go back and rewrite the statements.

There is one blockchain, though, to which these concerns do not apply: Aptos. Let’s see why formal verification on Aptos is much easier and cheaper.

Formal verification in Aptos: Move prover

Move smart contracts are perhaps better suited for formal verification than those in any other blockchain programming language. That’s because it comes with Move Prover – a fast automated tool that was developed together with the Move language.

In fact, apart fro the standard variety of Move, there is another one: Move Specification Language, or MSL. It is designed for representing contract code in the form of statements that the Prover understands. Having a special sublanguage for writing formal specification simplifies verification enormously. Here is an example of MSL in action:

Read more about Move Specification Language here

Like other formal verification prover tools, Move Prover checks if the formal model of a smart contract satisfies the specification for all possible values of the variables. If it finds a situation where this doesn’t hold true, Prover provides a counter-example, or a set of variable values for which the contract doesn’t satisfy the specification requirements.

Formal verification of Liquidswap: a big step forward for Pontem

To verify Liquidswap, we have partnered up with the leading experts in formal verification for Aptos, MoveBit. They previously helped create formal specifications for the Aptos Framework itself on behalf of Aptos Foundation.

Read the formal verification report by MoveBit

In this instance, we focused on the concentrated liquidity module as the most complex and the least tested. A total of six Liquidswap contracts underwent formal verification, as well as manual code analysis:

1. lb_token.move
2. pool.move
3. oracle.move
4. treasury.move
5. config.move
6. emergency.move

Only two issues were discovered in all of six contracts, and only one of them required the attention of the Pontem team. It concerned the allowed balances of tokens in a pool after a swap, and we fixed the issue straight away.

In the report file, you will find a list of contract functions that were verified, as well as descriptions of the properties (how the contracts should behave), for example: “the pool must contain both tokens during the swap” - and how they were verified (formally or manually).

Pontem Network has become one of the first on Aptos to formally verify one of its dApps. Once again, we act as pioneers in the space, setting the standard for other protocols. By proving formally that Liquidswap’s code (in particular, the CLMM module) does not contain vulnerabilities, we have offered the highest possible level of security assurance to our users.

This isn’t the end of the road security-wise: we hope to continue with formal verification of other models and products by Pontem. Keep following our security updates in this blog!