安全性、測試與形式化驗證

我們是 Runtime Verification，一家致力於建構嚴謹工具以確保關鍵系統安全性和正確性的研發公司。我們的團隊開發了 KEVM，這是以太坊虛擬機 (EVM) 最完整且經過實戰測試的形式語義，使用 K Framework 編寫。 KEVM 不僅僅是一個規範，它是一個可執行的規範，可用於對智能合約進行符號推理、執行一致性測試、分析 gas 使用量、對程式進行除錯，並形式化驗證正確性屬性。它通過了完整的以太坊測試套件，並用於驗證高價值合約，包括 Solidity 和 Vyper 中的 ERC-20 代幣。我們最近更新了語義以支援 Pectra 升級。 KEVM 正被 Kontrol 積極利用——這是我們的 Solidity 形式化驗證工具，被 EVM 生態系統中的領先團隊積極使用，包括 Optimism、以太坊基金會 (Ethereum Foundation)、Lido、Uniswap，以及更廣泛的以太坊社群中的安全研究人員和稽核員。 我們積極維護此儲存庫，為以太坊的協定演進做出貢獻，並與 Foundry 等開發人員工具整合。透過 KEVM，我們正在突破可證明正確且安全的智能合約基礎設施的極限。

Act 是一種用於形式化驗證的智能合約規範語言和工具包。Act 規範是對 EVM 程式所有可能行為的形式化高階描述。Act 允許利用許多現有的通用驗證工具來證明關於規範的屬性。這些工具包括 SMT 求解器（cvc5、z3、bitwuzla）、定理證明器（Coq）和經濟分析工具（CheckMate、Open Games）。Act 規範可以自動證明與 EVM 中的具體實作等效。對於非常簡單的合約，可以從 EVM 位元組碼自動產生 Act 規範。 這是一個端到端的管道，支援對 EVM 位元組碼高階屬性進行有原則的推理。它支援對正確性（例如會計不變數）和經濟屬性（例如誘因相容性）的推理。Act 規範作為高階智能合約表示，允許將現有的通用分析和驗證工具輕鬆整合到 EVM 環境中。

Titanoboa 是一個 Vyper 直譯器和測試框架，為 Vyper 智能合約提供現代化、整合的開發體驗。它使開發人員能夠直接在 Python 中測試和除錯 Vyper 合約，提供漂亮的追溯 (tracebacks)、分叉 (forking)、除錯功能、pytest 整合和開箱即用的模糊測試等功能。除了其獨立功能外，Titanoboa 還作為 Ape 和 Moccasin 等其他流行測試框架的基礎，並且是 Vyper 生態系統的核心基礎設施。