# Audits & Formal Verification ### Security Reports * [ChainSecurity Curve & Convex Audit Report](https://drive.google.com/file/d/1h-vjVceL2k03jXAN_mBcEmeUbATcrrEt/view?usp=sharing) * [Certora Formal Verification Report of Silo Protocol](https://drive.google.com/file/d/1D2EIOb0XaRov5Ph2AE0DTfIsMISd7UXG/view?usp=sharing) * [Certora Formal Verification Report of Chainlink Price Provider](https://prover.certora.com/output/74264/b233863cce92448566db?anonymousKey=2a3af53f3a3da84fa1a7763b6122b1d9c32caf32) * [ABDK Audit Report](https://drive.google.com/file/d/1WXaB3ICLv4rSEX86POK3-NaOIxXwyq9l/view?usp=sharing) * [Quantstamp Audit Report](https://drive.google.com/file/d/10GyfA-nBJ5jqLWW9LEYJQeFem8qSgNH6/view?usp=sharing) ### Important Information About Audits {% hint style="warning" %} Silo v1.1.1 was fully audited by QS and ABDK. Deployed version differs from the audited version. All Silo versions are formally verified. Read on. {% endhint %} The core contributors team followed rigid processes to develop and secure the Silo protocol, including: * Writing comprehensive unit tests * Verifying contracts against written rules (a process known as Formal Verification) * Conducting extensive internal code reviews * Hiring two reputable auditors to audit contracts * Running a [security bounty program](/security/bug-bounty-program.md) through Immunefi Silo v1.1.1 refers to core smart contracts that implement permissionless isolated lending markets governed by the Silo DAO. Version v1.1.1 was fully audited by Quantstamp and ABDK. Upon the conclusion of the audits, the core team tested audited contracts against various formal verification rules using the Certora Prover (the process is known as Formal Verification). The [Formal Verification revealed](https://drive.google.com/file/d/1D2EIOb0XaRov5Ph2AE0DTfIsMISd7UXG/view?usp=sharing) a few critical vulnerabilities that went undiscovered in both the ABDK and Quantstamp formal audits. The team fixed those vulnerabilities and released a new version of smart contracts. Rather than repeating the full audit again, the team extensively reviewed the code and tested it against formal verification rules. Smart contracts pass all Formal Verification specifications. Please see the Formal Verification report While we believe the audited version Silo v1.1.1 and deployed version do not vary materially, we cannot guarantee the security of any shipped deployments including the currently deployed version. Going forward, the core team will only audit new versions of the protocol–that is, when there are major upgrades to the architecture of the protocol. The core team has already retained Trail of Bits to audit Silo V2. Silo beta imposes deposit caps in launched markets (Silos) to limit users’ exposure. During the first 4 weeks of beta, the core team will work with the white hats community through Silo’s bounty program to further improve the protocol’s security. --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://devdocs.silo.finance/security/audits-and-formal-verification.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.