Introduction

[lucasmt]

_audits_lidofinance_dual-governance_fork/test/kontrol/report/DualGovernanceFormalVerificationReport.md

Lines 7 to 19 in dfe0fce

	Lido has engaged Runtime Verification to formally verify correctness and safety properties of the smart contracts that comprise the Lido Dual Governance protocol. The formal verification was conducted using Runtime Verification's symbolic execution tool Kontrol. Kontrol's symbolic execution is performed over the compiled EVM bytecode of the smart contracts, thus guaranteeing that it can catch errors introduced by the compiler or identify corner cases that may not be evident on source code inspection.
	The formal verification of the Dual Governance contracts was performed over the following commit: https://github.com/lidofinance/dual-governance/commit/3e0f1ae5740ef8410e928f6cc106e3a5f45a5a75. The contracts were compiled using Solidity v0.8.26, and the Kontrol version used was v1.0.118.
	All Kontrol tests described in this report have passed in the above commit. The full formal verification results, including running time information for the symbolic execution of each test, can be seen in Runtime Verification's [KaaS](https://kaas.runtimeverification.com/) platform for cloud-based symbolic execution:
	* `RageQuitTest`, `VetoCooldownTest`, `EscrowAccountingTest`, `EscrowOperationsTest` and `ProposalOperationsTest`: https://kaas.runtimeverification.com/job/c2e99782-183f-435c-9623-603d09088367/xml-report
	* `EscrowLockUnlockTest` (`testLockStEth`): https://kaas.runtimeverification.com/job/e8ad2685-57ba-4d56-b587-caadab40f3fa/xml-report
	* `EscrowLockUnlockTest` (`testUnlockStEth`): https://kaas.runtimeverification.com/job/415b46c2-c4ec-4d72-af6c-28e72f26f64f/xml-report
	* `TimelockInvariantsTest` and `TimelockedGovernanceTest`: https://kaas.runtimeverification.com/job/0c503cbf-3f7b-46f2-8bf9-03a19e75f33c/xml-report
	* `VetoSignallingTest`: https://kaas.runtimeverification.com/job/f86e31cd-51ef-4cfd-9cd0-0288568948b0/xml-report
	These results have also been collected in the accompanying [KaaS report](https://github.com/runtimeverification/_audits_lidofinance_dual-governance_fork/blob/kontrol-formal-verification/test/kontrol/report/DualGovernanceFormalVerificationReport_KaaS.pdf).