Security
SMTChecker 和 Manticore 的區別？
為什麼我要使用 Trail of Bits 的Manticore而不是SMTChecker，它是在 Solidity 編譯器中烘焙的？
tl;博士：你應該同時使用（以及更多）:)
不同的 FV/靜態分析工具通常具有不同的功能和優缺點，它們可能相互補充並為您提供更好的覆蓋範圍。
例如，在這種情況下，Manticore 以 EVM 字節碼為目標，而 SMTChecker 以 Solidity 程式碼為目標。
- 以 Solidity 為目標更適合高級屬性、契約不變數和直接推理狀態變數。SMTChecker 擅長合約不變數，可以處理循環並在可讀的 Solidity 級別（全自動化）上為屬性（錯誤）提供反例，但在證明低級別屬性、按位操作、內聯彙編和低級別數據操作時通常會失敗.
- 針對 EVM 字節碼的工具通常是相反的。我不能完全代表 Manticore，但hevm就是這種模式的一個例子。EVM 字節碼工具的一大特點是它們準確分析將要部署的內容，因此不需要信任編譯器（如 SMTChecker 所做的那樣），而是驗證編譯器的工作。其中一個例子是 EVM 字節碼包含 ABI 編碼/解碼程式碼，這些工具通常會針對特定合約進行驗證。分析 Solidity 的工具沒有這些，需要在輸入函式時假設編碼是正確的。從這個意義上說，EVM 字節碼工具提供的證明更強大。
除了基本的符號編碼/證明技術外，每個工具都有自己的一組功能，這些功能可能對您的情況有用或無用。這是我嘗試保持更新的更多工具的列表： https ://github.com/leonardoalt/ethereum_formal_verification_overview