從 Detect 到 Proof：智慧合約審計工具實戰 系列

審計工具沒有報錯，合約就安全了嗎？本系列以 DeFiHackLabs 公開的真實案例為題材，依序使用 Slither 靜態分析、Foundry 動態測試與 Certora Rule 形式化驗證，比較不同方法能發現什麼、需要哪些前提，以及為何可能誤報或漏報。最後討論 LLM 在審計流程中的角色，整理出一套從 Detect 到 Prove 的實作方法。