Hello! My name is Kirill Ziborov, and I’m a formal verification engineer and security researcher at Positive Web3. From February 24 to March 18, an audit contest for the Blend protocol on the Stellar blockchain was held on the Code4rena. In addition to the traditional manual audit, the competition included a formal verification track using the Certora Sunbeam Prover. This was the first contest of its kind on the Stellar blockchain, and our team placed 4th. In this article, I want to share my experience and impressions of the tool, as well as discuss formal verification of smart contracts on the Stellar blockchain in general.
Introduction
In my previous article, I described what formal verification of smart contracts is and its value in the context of blockchain security. Briefly, formal verification is a set of mathematical methods that ensure a program meets a given specification. In that article, I used the ConCert framework, implemented on top of the Coq (Rocq) proof assistant, for interactive proof of properties of a DEX/AMM protocol written in Solidity. During an interactive proof in proof assistants, the engineer writes formal specifications as theorems and proves them using tactics, which are interactively checked by the proof checker.
In contrast, Certora’s tools allow security researchers the ability to automatically check formal specifications. Many readers have probably heard of the Certora Prover for Ethereum and Solana smart contracts. This tool is already actively used by many auditors and has been competitively applied in public audit contests for protocols such as Euler, Uniswap v4, and Aave. If not, you can get acquainted with it in detail using the developer article and documentation. To verify a property of a Solidity smart contract with Prover, the engine
[…]
Content was cut in order to protect the source.Please visit the source for the rest of the article.
Read the original article: