TLDR: Greater assurance for Milkomeda! We have worked with Certora to formally verify the Solidity smart contracts on the EVM side of the Milkomeda bridge. Read the report here.

The importance of security in the blockchain world cannot be understated, and it is something we take very seriously at Milkomeda. With the growth of blockchain interoperability, blockchain bridges have become a big value target for hackers.

We’ve already completed audits of elements of the Milkomeda bridge, and now we are proud to announce that we have done something very few other protocols have done: we have just completed a formal verification of the Solidity smart contracts on the Milkomeda side of the bridge!

This article will explain what formal verification is, what it can do for smart contracts, and how it compares to manual processes. We will then discuss the outcome of the formal verification of Milkomeda’s bridge contracts.

Note: This undertaking is only for the Solidity contracts on the Milkomeda side of the bridge.

What is Formal Verification?

Formal verification is a highly recommended way of enhancing smart contract security. It uses formal methods to verify that a smart contract performs as it was designed to. Formal methods use a combination of math and logic to create an abstract representation of the code and reason about it, typically by comparing it to another formal description called the formal specification.

This allows a smart contract to be evaluated for correctness — its ability to behave as intended — with respect to a particular formal specification. The specification is made up of a series of statements, written in a formal language, that describe the intended execution paths of the smart contract.

A verification tool is given both the mathematical representation of the code and the formal specification, and it searches for behaviors or outputs that do not follow the path described by the specification. The verification tool manipulates logical formulas to reason about the contract’s behavior on an infinite range of inputs, thus determining whether the contract is always valid or if there is an input that violates the contract’s intended purpose.

There are multiple open source tools for formal verification, as well as professional companies that have their own proprietary tools. We worked with the skilled professionals at Certora to conduct the formal verification of the Milkomeda smart contracts. Their clients include some of the biggest names in the DeFi world, as well as L1-L2 bridges for EVM-based protocols, with over $32B in TVL protected by the formal verification undertaken by Certora. You can read more about how their suite of tools works in their whitepaper.

Formal Verification vs Auditing and Manual Methods

While manual audits and testing are an important part of smart contract security, there are major limitations to human-based methods that are overcome by formal verification. Formal methods can verify smart contract behavior for an infinite number of execution paths, often finding an input or rare behavior that results in a bug — a level of testing that is not feasible when done manually. Working with formulas rather than concrete inputs also means that the verification tool follows every possible state that a contract could be in, allowing it to flag any issues that may not be immediately obvious.

In contrast, manual audits and testing can only consider a finite number of inputs and execution paths, making it more likely that a bug will be missed. Manual methods also rely on the expertise and attention to detail of the auditor, which can vary from person to person.

The outcome of the Formal Verification of Milkomeda’s Bridge Contracts

The formal verification of the Milkomeda bridge contracts was a success. The process resulted in the identification of several issues that were addressed and fixed before the contracts were deployed. The formal verification process provided greater assurance of the security of the Milkomeda bridge contracts and allowed us to have confidence in their reliability and functionality.

We highly recommend formal verification for any smart contracts that handle significant value or have a complex structure. While it is an additional step in the development process, the increased security and assurance it provides are well worth the effort.

Milkomeda’s Solidity Smart Contracts are Now Formally Verified!

We are pleased to have completed the formal verification of the Milkomeda bridge contracts and will continue to prioritize security in all of our developments. We hope that this article has provided some insight into the benefits of formal verification and its importance in the blockchain world.

The formal verification of our Solidity smart contracts is just one of the steps down the road in the continued growth of the Milkomeda protocol. Be sure to follow us on your chosen channel to keep up with all the updates we have coming in another exciting and groundbreaking year!