Certora Formal Verification
We at Saddle are happy to release the result of the formal verification by Certora performed to mitigate potential risks, vulnerabilities, and bugs in the contract Swap.sol
The formal verification was done as part of Saddle's commitment to enhance protocol security and mitigate the possibility of catastrophic bugs. Even the slightest vulnerabilities can cause significant losses, so it is imperative to implement robust security measures and adopt sophisticated tools and strategies to eliminate potential risks. At Saddle, we take the security of our smart contracts extremely seriously to safeguard our users' funds and protect their interests.
A security company focused on checking code correctness in smart contracts, Certora helps developers detect and prevent security mistakes before code is deployed. Certora offers formal verification, a powerful method to mathematically ascertain the code adheres to the outlined specifications.
Formal verification utilizes mathematical models and computer algorithms to improve the security of smart contracts by identifying and preventing security bugs in the implementation. Certora has successfully identified bugs and strengthened the security of the most significant protocols in DeFi, including Aave, Compound, Notional, and Bancor.
This announcement briefly overviews the report. For a detailed analysis, check out the formal verification here.
Brief Overview
Saddle engaged the services of Certora as a mechanism to secure the Swap.sol smart contracts. A prover such as Certora’s is the best way to verify program correctness. Math and logic prove effective in early bug detection, and Saddle wanted to ensure the program behaves appropriately before deployment.
The goal was to thoroughly analyze the code and specifications to ensure no violating scenarios (where the code deviates from the specification). This was deemed essential by the Saddle team to enhance code security and locate critical vulnerabilities if any.
The scope of the verification was Saddles’s contract Swap.sol. The Certora Prover proved the contract implementation is correct with respect to the formal specifications written by Saddle and Certora teams. The formal specifications focused on validating correct behavior for Swap.sol as described by our team and the contract documentation. The rules verify valid states for the system, proper transitions between states, method integrity, and high-level properties. Shoutout to Hannes on the Saddle team for his thoughtful work on this project!
Conclusion
A verification tool from Certora’s suite of offerings complements manual audits and bug bounties. Our priority is customer safety, and are pleased to announce that Certora Prover supports the finding that Swap.sol smart contracts fulfill their intended purpose.
Additionally, we will continue our efforts to protect our users from losses that suffice from inefficient logic or incorrect code.
About Certora
Certora is a leading provider of technology and services for eliminating vulnerabilities in smart contracts.
About Saddle
Saddle Finance is a decentralized AMM that enables cheap, efficient, fast, and low-slippage swaps. Saddle is built by a team of DeFi natives aimed to bridge the gaps between the different silos of DeFi. We believe in collaboration, building Saddle as a DeFi lego block, and helping DeFi teams bring AMMs to any blockchain.
Feel free to reach out through our community Discord or follow us on Twitter.