This report presents the findings from the formal verification of the Lido Dual Governance protocol, conducted by Runtime Verification on behalf of Lido. The objective of this verification was to assess the correctness and safety of the smart contracts that constitute the protocol, ensuring they operate as intended under various conditions. This verification was crucial for Lido to maintain the integrity and security of its Dual Governance system, which plays a significant role in the protocol's overall functionality and security posture.

The formal verification process employed by Runtime Verification utilized Kontrol, a sophisticated tool designed for the symbolic execution of Solidity smart contracts. Kontrol operates by executing the compiled EVM bytecode of the smart contracts, allowing it to identify potential errors introduced during the compilation process or uncover corner cases not immediately apparent through source code inspection. This approach ensures a comprehensive examination of the smart contracts beyond traditional testing methodologies. Key Findings: - The formal verification process involved rigorous testing of various components of the Lido Dual Governance protocol. This included the EscrowLockUnlockTest, TimelockInvariantsTest, TimelockedGovernanceTest, and VetoSignallingTest. Each of these tests was aimed at validating specific aspects of the protocol's functionality and security mechanisms.

The results, compiled in the accompanying KaaS report, indicate that the Lido Dual Governance protocol's smart contracts are correctly implemented and adhere to the specified safety properties. These findings suggest a high level of assurance in the protocol's ability to function as intended, mitigating the risk of unintended behaviors or vulnerabilities. - It is important to note that while the formal verification process provides significant insights into the protocol's reliability, it does not eliminate all potential risks. Users and stakeholders are advised to engage with the protocol and this report with an understanding of the inherent uncertainties associated with new and emerging technologies.