Formatted output from test__DOSStethHyperdriveCloseLong Running 1 test for test/integrations/StethHyperdrive.t.sol:StethHyperdriveTest [PASS] test__DOSStethHyperdriveCloseLong() (gas: 676273) Logs: ########################################################################### #### TEST: Denial of Service when LIDO's `TotalPooledEther` decreases. #### ###########################################################################

Certora Summary This document describes the specification and verification of OpenZeppelin's contracts using the Certora Prover. The work was undertaken from May 9th to June 10th. The latest commit that was reviewed and run through the Certora Prover was commit 109778c. The scope of our verification was the following contracts: Initializable.sol ( Verification Result ) GovernorPreventLateQuorum.sol ( Verification Result ) ERC1155Burnable.sol ( Verification Result )

Certora Summary This document describes the specification and verification of Aave's V3 protocol using the Certora Prover. The work was undertaken from Nov. 12, 2021 to Jan. 24, 2022. The latest commit that was reviewed and ran through the Certora Prover was a87d546. The scope of this verification is Aave's governance system, particularly the following contracts: StableDebtToken.sol ( Verification Results ) VariableDebtToken.sol ( Verification Results ) Atoken.sol (Verification Results)

June 20, 2022 Certora is building a developer tool for smart contracts that supports finding bugs, reasoning about correctness, and producing formally verified proofs. The framework consists of two main components: (1) a specification language for describing intended smart contract behaviors symbolically and (2) an engine for analyzing the smart contracts against the specification. The technology automatically locates critical bugs that even the best auditor can miss and increases confidence in code security by proving that certain rules hold. On a high level, the Certora prover is essentially a sophisticated compiler translating the bytecode and the properties into a mathematical formula that concisely defines the exact conditions under which the program may violate the properties. This formula is fed into existing open source tools which locate bugs and produce proofs. This document describes the main techniques implemented in the Certora Prover from a high-level perspective. We assume that the readers are familiar with smart contracts. The examples used in this document are also accessible at Certora's demo page. Design Principles The Certora prover takes a low-level EVM bytecode program and a specification written in Certora's specification language, CVL.[^1] The prover analyzes the code and the spec together to identify scenarios where the code deviates from the specification.

Summary This document describes the specification and verification of OpenZeppelin's contracts using the Certora Prover. The work was undertaken from March 2 to April 6, 2022. The latest commit that was reviewed and ran through the Certora Prover was 4088540a. The scope of this verification is OpenZeppelin's governance system, particularly the following contracts: ERC20Votes.sol ERC20FlashMint.sol ERC20Wrapper.sol TimelockController.sol draft-ERC721Votes.sol

DeFi and the risks of smart contract bugs Only a few days ago, Akudreams—an NFT project from former baseball player Micah Johnson—suffered a failure on launch when $34m of the founders' stake was locked up forever due to a bug in smart contract code. Decentralized finance, or DeFi, promises all kinds of transactions—loans, payments, trading, auctions, insurance, etc.—but without banks or any centralized authority. Eliminating the need to trust any such authority, along with prejudices that have favored some clients over others, is key to the success of DeFi. Contracts negotiated and interpreted by humans are replaced by smart contracts, computer programs that operate with perfect objectivity. The very objectivity of such contracts, however, makes them, and those who participate in them, vulnerable to subtle errors in the code. The AkuDreams debacle is only the latest of a series of smart contract disasters. Back in mid-2016, the DAO, a kind of decentralized venture-capital fund, lost a third of its investment value when a hacker exploited a smart contract bug. Why smart contract bugs are different

Summary This document describes the specification and verification of ConstantProductPool by SushiSwap using the Certora Prover. The work was undertaken while the contract was in development and concluded on Nov 4th, 2021. The scope of our verification was ConstantProductPool contract, a liquidity pool that uses a constant product market maker and consists of two tokens. The LP tokens are called Trident tokens. The Certora Prover proved the implementation of ConstantProductPool is correct with respect to the formal rules written by the Certora and SushiSwap team. The next section formally defines high level specifications of ConstantProductPool. The results of running the Certora Prover are available at: ConstantProductPool

Summary This document describes the specification and verification of TridentRouter by SushiSwap using the Certora Prover. The work was undertaken while the contract was in development and concluded on Nov 4th, 2021. The scope of our verification was TridentRouter contract. It is a router contract that helps to swap, mint, and burn across Trident pools. The Certora Prover proved the implementation of TridentRouter is correct with respect to the formal rules written by the Certora and SushiSwap team. The next section formally defines high-level specifications of TridentRouter. The results of running the Certora Prover are available at: TridentRouter

Summary This document describes the specification and verification of Rolla Protocol using the Certora Prover. The work was undertaken from June 7 - 24, 2021. The rules are running as part of CI. The scope of our verification was the Controller, CollateralToken and FundsCalculator contracts. The Certora Prover proved the implementation of the Rolla Protocol is correct with respect to the formal rules written by the Rolla team and the Certora teams. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. All issues were promptly corrected, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The Certora development team is currently handling these limitations. The next section formally defines high level specifications of Rolla Protocol. All the rules are publically available in a public github. Certora Prover run results:

Summary This document describes the specification and verification of Zesty Market using the Certora Prover. The work was undertaken from June 21, 2021 to July 4, 2021. All commits are run through the Certora Prover. The scope of our verification was the Zesty Markets logic. The Certora Prover proved the implementation of the Zesty Market is correct with respect to the formal rules written by the Zesty and the Certora teams. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. All issues were promptly corrected, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The Certora development team is currently handling these limitations. The next section formally defines high level specifications of Zesty. All the rules are publically available. Certora Prover run results: Zesty Market V1_1