領先的區塊鏈安全平台Certora開源了其最先進的形式驗證引擎 Certora Prover，以使加密貨幣行業的每個人都更容易獲得智慧合約安全性。
隨著駭客在數位資產領域激增並竊取資金，Certora 的這一舉措來得正是時候。
「安全性仍然是 Web3 面臨的最大挑戰之一。 Certora 技術長 Shelly Grossman 指出，DeFi 專案花費數百萬美元進行審計，通常需要一年多的時間才能啟動，但漏洞仍然使數十億美元面臨風險。今天一切都變了。
區塊鏈分析公司 Chainaanalysis 的數據顯示，2024 年駭客竊取了高達22 億美元的資金，比一年前成長了 21%。不僅金額增加，事件數量也增加。
隨著加密貨幣採用率的增加，在零售店和機構中越來越受歡迎，以及加密貨幣總市值超過3 兆美元的市場爆炸式增長，不良行為者肯定會倍增。這些網路犯罪分子正在採用越來越複雜的方法，並透過利用智慧合約的弱點來擴大其影響範圍，而智慧合約是 DeFi 協定和生態系統的支柱。
在這種背景下，Certora 為 DeFi 開發人員提供了一個強大的解決方案，它可以識別所有可能的錯誤，然後證明它們不存在。支持更流行的連鎖店，即以太坊 (EVM)、Solana (sBPF) 和 Stellar (WASM)、Certora 確保絕大多數加密空間免受智慧合約攻擊。
Prover是Certora的旗艦安全產品，它使用形式化驗證來發現最困難和罕見的錯誤。經過「長時間」的生產，該樂器終於向公眾發布。
Certora Prover 本質上充當自動數學審計員，分析智慧合約程式碼和開發人員定義的規則以提供正確性證明。透過這種方式，我們超越了有限的場景，評估每一種可能的情況。開發者已經編寫了超過70,000條驗證規則。
實際上，借助 Certora 的形式化驗證技術，最終發現了 MakerDAO 的 DAI 方程中的一個基本缺陷，該缺陷自 2018 年以來一直沒有被發現。
借助該工具，Cetora 還幫助 Aave、Uniswap、Lido、EigenLayer、Solana Foundation 等公司獲得了數百億美元的 TVL。
然而，Certora 一直擁有自己的閉源代碼，最終發生變化，為所有 Web3 開發人員提供一個強大且完全免費的工具，以確保他們的智能合約安全、透明且由社區驅動。
「智能合約安全不應該是資金充足的團隊或受過高等教育的個人的特權。 Certora Prover 的開源讓防彈智能合約成為常態又更近了一步。
Certora 免費向所有人開放，目前正在邀請開發人員、安全研究人員和 Web3 社群使用該解決方案來驗證其智能合約，並協助推進其保護 DeFi 的工作。