Mathematically-Proven: Uniswap V3's Formal Verification by MetaTrust Labs

MetaTrust Labs recently completed the first formal verification of Uniswap V3 Swap protocol in response to the request from Xcalibyte. The verification rigorously analyzed Uniswap's source code and mathematically proved it correctly implements the intended financial model described in the Uniswap V3 whitepaper.

To verify Uniswap's complex code and model, MetaTrust Labs leveraged an innovative analysis tool they developed. Here is how the verification was done according to the team.

As part of our research on Web 3.0 security, we conducted a formal verification of a large portion of Uniswap V3.

We first constructed a formal model of the Uniswap V3 source code using the specification language supported by our verification tool.

Second, we furnished the Uniswap formal model with properties it must satisfy, using the logic defined by our tool. These properties formalize the financial model described in the Uniswap V3 white paper, involving complex mathematical concepts like discrete integrals.

Due to the sophisticated nature of Uniswap V3's financial model, standard verification tools cannot prove the Uniswap code correctly represents its mathematical model. Our tool uses cutting-edge verification techniques and new mechanisms to specify and verify such a complex system.

Technically, the tool employs Separation Logic enhanced with Data Refinement to enable automatic verification, all developed using the Isabelle/HOL theorem prover. Using a theorem prover ensures the tool itself has been fully formalized mathematically.

Compared to existing methods, first, the theorem prover provides a minimal trusted base for verification at the state of the art. Second, logic formalized in an expressive theorem prover allows our tool to specify and verify high-level properties of financial models, like the discrete integral described in the Uniswap V3 white paper.

The success highlights the value of custom verification tools in auditing sophisticated DeFi systems. Mathematically-grounded verification is enabling the next generation of trusted and widely used DApps.

"We are proud to provide the analysis capabilities instrumental in this significant achievement. Formal verification at this level sets a new standard for transparency and reliability in blockchain software," said David from MetaTrust Lab.

The first formal verification of Uniswap V3 Swap protocol is a breakthrough for the DeFi ecosystem and a model for future collaborations, and this has given Uniswap users more reason to trust and adopt its platform.