This document describes the specification and verification of BENQI's Liquid Staking system using the Certora Prover. The work was undertaken from March 14, 2022 to April 14, 2022.

The Certora team verified the code that was delivered to us on February 23, 2022. The scope of our verification is the Liquid Staking system, defined in the StakedAvax contract.

The Certora Prover proved the implementation of Benqi's StakedAvax contract is correct with respect to the formal rules written by the Certora team.