原文來源：Beosin
近年來，GPT-4、Claude、Gemini 等大語言模型已經具備較強的代碼理解能力，能夠較好地閱讀 Solidity、Rust、Go 等智能合約語言，也能識別重入攻擊、整數溢出等具有明顯代碼特徵的經典漏洞。這讓行業開始思考：是否可以用大模型來輔助甚至替代人工進行合約審計？
由於通用模型對具體項目的業務邏輯瞭解不足，在面對複雜的DeFi 協議時，誤報率較高，也容易漏掉那些需要結合跨合約交互或經濟模型才能發現的漏洞。後來，業界提出了加入“Skill”機制的方案——在通用大模型的基礎上，注入針對智能合約安全的專項知識庫、檢測規則和業務上下文，讓模型在審計時有更明確的判斷依據，而不是僅靠通用能力去判斷代碼是否存在問題。
即便加入 Skill 增強，AI 審計仍然有明確的適用範圍。它擅長已知漏洞模式的掃描和代碼規範檢查，但對於需要深入理解整體協議設計、跨合約交互邏輯或經濟模型的複雜漏洞，目前仍難以有效處理。這類問題仍然需要經驗豐富的審計專家來負責，而在涉及複雜計算邏輯的場景中，還需要引入形式化驗證提供更強的保障。在此背景下，Beosin 構建了 Skill 增強 AI 基線檢查 + 人工深度審計 + 形式化驗證的三審計模式，三者各有側重、互為補充。
一、通用AI模型的審計能力邊界：受控對比測試與案例分析
本文從已完成人工審計的項目庫裡，選取了兩類複雜度差別較大的合約來做測試案例：一類是邏輯比較獨立、功能邊界清晰的簡單合約，這類項目通常是AI 審計工具訓練數據最充足、理論上最佔優勢的場景；另一類則是涉及多合約交互、複雜狀態機或者跨協議依賴的複雜合約，這也正是行業裡討論“AI 能不能替代人工審計”時，最常被拿出來說的高風險場景。
在對比時，我們用完全一樣的代碼庫，先讓 AI 獨立跑一遍審計，生成報告後再和人工審計報告一條一條對齊。兩份報告的產出過程完全互不干擾——人工審計員出報告時根本不知道 AI 的結果，避免相互影響。最後，我們會從以下四個維度來分析結果：
案例 A · 標準代幣合約（BSC-USDT / BEP20USDT.sol）
第一組測試，我們選取了一個標準的 BEP-20 代幣合約，使用 Solidity 0.5.16 編寫。它的邏輯相對獨立，功能邊界很清晰，沒有涉及任何跨合約交互，主要的安全風險都集中在一些常見的、已知的漏洞模式上。這類合約目前理論上是 AI 審計最佔優勢的場景——訓練數據裡這類標準代幣合約非常多，規則性的漏洞特徵也比較明顯。
AI 共輸出 6 項告警（2 高危、1 中危、3 低危/建議），從數量上看較為可觀。低危與建議項基本準確，覆蓋了 Solidity 版本過舊、狀態變量暴露方式等常見代碼規範問題，具有一定參考價值。然而，AI 輸出的兩項"高危"均構成誤判。AI 將 owner 鑄幣權和權限集中標記為高危漏洞——實際上對於中心化穩定幣（USDT 類），owner 擁有鑄幣權屬於預期設計，風險評估應結合多籤控制、權限治理機制及合約升級策略綜合判斷。這類權限結構的合理性，根本上取決於項目的業務模型而非代碼本身，AI 缺乏這一層語境，只能基於模式匹配做出判斷。
該測試案例顯示，AI 能識別權限結構，但無法結合業務語境判斷權限是否合理，所以將 USDT 類合約的 owner 鑄幣權直接標記為"高危漏洞"，這是典型的脫離業務實際邏輯的誤判——這類誤報可能干擾項目方對真實風險的判斷。
案例 B · 複雜業務合約（IPC Protocol / 2025-02-recall）
第二組測試選取 Code4rena 平臺公開報告中的 IPC Protocol 項目（報告鏈接：code4rena.com/reports/2025-02-recall）。該項目包含 Gateway、SubnetActor、Diamond 代理模式等多個相互依賴的核心組件，安全性高度依賴對協議整體架構和跨組件交互邏輯的深度理解，這是 DeFi 生態中高價值攻擊的典型發生場景。下面是AI審計結果：
針對複雜合約，AI 審計共產出 3 項高危、6 項中危告警，從輸出體量上並不遜色。但其中相當比例被審計員判定為誤報——AI 對缺乏上下文的代碼片段做出了錯誤的風險判斷。與此同時，在審計員確認的 9 個 High 級漏洞中，AI 僅完整覆蓋 1 項，另有 2 項被發現但定級明顯偏低（實為 High，AI 報告為 Medium），其餘 6 項完全未被發現。4 個 Medium 級漏洞中，AI 覆蓋了 1 項，3 項完全缺失。
這些漏洞的共同特點是：都依賴對協議跨組件狀態轉變路徑的完整推理，而非對單一函數的模式匹配。以人工審計報告中的 H-01（簽名重放）為例，漏洞的利用路徑需要理解多籤驗證的設計意圖、攻擊者如何構造重複簽名集合、以及這一行為如何繞過權重閾值。H-06（leave() 函數重入攻擊）同樣如此：漏洞僅在子網 bootstrap 臨界狀態下存在，需要理解質押流轉、bootstrap 觸發條件與外部調用時序三者之間的交叉依賴。類似的深層邏輯漏洞，在 AI 的告警列表中沒有任何記錄。
該結果顯示在複雜合約審計中：AI 的審計能力在於局部代碼的模式識別，而協議級漏洞可能存在對整體業務邏輯的理解偏差。當漏洞的觸發條件跨越多個合約、多個狀態、多個調用層級時，AI 當前的推理能力尚無法有效覆蓋。
綜合兩個案例來看，AI 審計並非沒有價值——它在已知漏洞模式的覆蓋、代碼規範檢查、以及部分獨立視角的發現上具有實質貢獻。但它的價值邊界非常清晰：可以作為基線掃描，但不能直接作為安全結論。對於複雜協議，僅依賴 AI 報告做出安全判斷，不僅會漏掉風險較高的漏洞，還會因為大量低質量告警佔用團隊大量篩查時間。這正是Beosin建立專屬Skill知識庫，以及在審計流程中引入三審計模式機制的核心原因。
二、專屬Skill知識庫：提升AI基線檢查的工程化路徑
為了將把AI 審計納入基線檢查的審計流程，就必須解決其在審計真實 DeFi 協議時誤報和漏報率偏高的問題。無論是權限管理、AMM 流動性機制、跨鏈橋的消息驗證，還是借貸協議的清算邏輯，AI 目前都只能根據代碼表面的特徵做簡單匹配，很難結合具體的業務場景和攻防邏輯來判斷一段代碼到底有沒有問題。解決這個問題的核心，是把審計專家多年積累的經驗以結構化的方式注入到 AI 的判斷過程中，讓它具備一定的業務理解能力。
但是需要明確的是，即使引入了Skill 增強，AI 在審計中的定位也不會改變。對於那些涉及多合約交互、經濟模型分析以及新型攻擊手法的複雜問題，人工審計依然不可替代。Skill 的作用，是在 AI 能處理的範圍內（比如識別常見漏洞模式，並有限地理解業務邏輯），把初步掃描的質量提升到一個真正有用的水平，為人工審計提供更有價值的初步結果，而不是製造出一堆需要反覆甄別的無效告警。
2.1 從審計實戰中提煉：Skill規則的構建機制
Beosin 的 Skill 知識庫，來源於超過 4000 個已完成人工審計的智能合約項目，由審計專家進行了大量歸納、總結，並逐條提煉和驗證整理而成。每一條規則的形成，都完整走完了從漏洞發現到規則落地的全過程：審計師在真實項目中發現安全問題後，會對攻擊路徑進行完整還原，深入分析根本成因，驗證修復方案是否有效，最終把這一整套攻防認知整理成帶有上下文判斷條件的規則條目，納入 Skill 庫，供後續審計調用。
以下為Skill庫中的其中一個規則樣本，包含漏洞模式、攻擊路徑、根本成因與修復建議四個維度上的結構：
[Beosin-AMM_Skill-1] 添加流動性檢測通過轉賬順序繞過
漏洞模式：合約通過檢查Pair中WBNB餘額是否超出儲備量（balanceOf >= reserve + required）判斷是否為添加流動性操作。該檢測依賴WBNB先於代幣到Pair的假設，但Router的addLiquidityETH函數固定先轉ERC-20代幣再轉WETH，且addLiquidity函數的轉賬順序由參數順序決定。
攻擊路徑：攻擊者只需使用addLiquidityETH（代幣固定先轉），或調用addLiquidity(Token, WBNB, ...)使Token先於WBNB轉入Pair。檢測時WBNB尚未到達，balanceOf == reserve，檢測函數返回false，從而完整繞過“no add liquidity”限制。
根本成因：基於Pair餘額快照的檢測方式，在設計層面本質上無法可靠地區分swap與add liquidity操作，屬於架構性缺陷而非實現Bug。
修復建議：改為禁止非白名單地址直接向Pair轉賬，所有交易通過合約內置函數完成，從架構層面根除餘額快照檢測的根本缺陷。
該規則並非對單一代碼模式的簡單標註，而是對一類攻擊的系統性梳理：觸發條件如何構成、攻擊者沿何路徑繞過檢測、檢測機制在哪個環節存在架構性缺陷，以及修復需要在哪個層面介入。
2.2 知識庫的覆蓋範圍
Beosin目前已形成覆蓋Web3主流技術棧的專項skill漏洞庫，包括Solidity、Rust、Motoko、FunC、Go及ZK等大類。其核心內容作為內部核心資產不對外公開，目錄結構如下：
每個專項庫下的Skill都按照漏洞類型分開管理，每一條規則都包含編號、觸發條件、攻擊路徑還原、上下文判斷邏輯以及修復建議。整個Skill庫會隨著每次新型攻擊事件的出現和審計實例的積累持續迭代，確保始終與鏈上真實的威脅環境保持同步。
2.3 Skill介入後的基線檢查質量對比
為量化Skill庫對基線掃描質量的實際影響，我們以第二章中的兩個測試案例為基準，在相同代碼庫上分別運行通用AI與Skill增強AI，並對結果進行逐項比對。
案例A · 標準代幣合約（BEP-20）對比結果：
案例B · 複雜業務合約（IPC Protocol）對比結果：
對比結果顯示，引入 Skill 後，兩類合約的檢測質量都有明顯提升。在標準代幣合約場景中，由於加入了業務語境判斷能力，高危誤報被徹底消除；在複雜業務合約場景中，已知漏洞模式的覆蓋率從 11% 提升到 44%，誤報率從約 55% 降到約 30%，嚴重等級判斷的準確性也顯著改善。這份報告可以作為基線檢查，幫助項目方提前瞭解代碼中存在的缺陷。雖然這些問題暫時不會直接造成資金損失，但對後續的項目維護和升級仍有重要的積極作用。
然而，數據也清晰地暴露了 AI 能力的固有邊界：即使加入 Skill 增強後，在複雜合約中 High 級漏洞的覆蓋率也僅達到 44%。那些需要跨合約狀態路徑推理、經濟激勵模型分析，或特定時序條件才能觸發的深層漏洞，仍然遠遠超出 AI 基線掃描的能力範圍。這正是我們在引入 Skill 增強之後，審計流程中依然保留完整人工審計環節的根本原因。
2.4 白皮書作為審計輸入：代碼實現與設計意圖的一致性核查
除了漏洞特徵庫之外，我們在審計流程中還增加了一項重要能力：把項目的白皮書作為額外輸入，讓 AI 對代碼實現與白皮書設計之間的一致性進行驗證。
具體來說，在代碼審計開始前，AI 會系統地解析項目的白皮書、技術規範和需求文檔，從中提取角色權限模型、核心業務流程、信任邊界定義以及預期行為約束，形成結構化的項目語境摘要。隨後，在整個代碼審計過程中，AI 會持續參照這個語境進行交叉比對。這一機制在實際使用中帶來了兩類很有價值的結果：
第一，對於代碼中看似存在風險的權限結構，如果白皮書中已經明確說明了其設計意圖和約束條件，AI 會據此調整判斷，從而有效減少這類誤報。
第二，如果代碼實現與白皮書的承諾存在明顯偏差，比如文檔中宣稱的滑點保護機制在代碼裡並未實現，或者治理流程的時間窗口約束沒有被正確執行，AI 就會據此發出告警。這類代碼與文檔不一致的問題，在常規代碼掃描中非常容易被忽略，但往往正是潛在的安全隱患所在，同時也幫助項目方儘可能避免，項目實際上線後出現與其預期並不相符的行為。
三、三重審計模式：協同構建智能合約安全的完整保障
智能合約一旦部署上鍊，任何漏洞的代價往往都是不可逆的。Beosin 以人工深度審計 + 形式化驗證作為合約審計的基礎，重點發現並報告那些已經可能導致資金損失或邏輯運行異常的問題。同時，我們引入了基於專屬 Skill 知識庫的增強 AI 基線檢查，幫助客戶更早地發現那些目前還只是缺陷、尚未造成實際危害的代碼問題。在此基礎上，Beosin 構建了人工深度審計 + 形式化驗證 + 增強 AI 基線檢查三審計模式，通過三者分層協作，形成覆蓋更全面的安全保障體系。
3.1 人工深度審計與形式化驗證：安全保障的核心支柱
人工審計的核心優勢在於對協議整體設計的深度理解，以及從攻擊者角度主動分析潛在風險。經驗豐富的審計專家負責對項目進行全面的協議級審計，包括跨合約交互邏輯的驗證、資金安全的攻擊面分析、協議在極端市場條件下的邏輯分析，以及對新型攻擊方式的識別與判斷。這種協議級的攻防理解高度依賴對Web3生態的長期積累與實戰經驗，是工具層面目前無法獨立完成的。
在此基礎上，Beosin 以內部工具鏈將人工審計的判斷結論轉化為可量化的數學保證。針對審計專家確認的核心業務邏輯，如：資金流轉、價格計算等最高風險的關鍵路徑，Beosin 將 LLM 驅動的形式化規範生成能力深度集成進內部驗證工具鏈，構建了「AI 規範生成 → 形式化窮舉驗證 → 反例驅動精化」的閉環引擎。工具鏈首先以 Beosin 積累的審計語料庫為知識底座，對人工確認的高風險路徑進行攻擊面建模，輔助生成形式化不變量與安全屬性規範的初始候選集；隨後，自動形式化驗證引擎對合約的完整狀態轉換空間進行窮舉驗證。當驗證引擎發現反例時，系統自動區分兩類情形：若反例源於規範定義與業務語義的偏差，則將反例上下文回傳 AI 模塊進行規範精化，驅動下一輪迭代；若反例對應合約代碼的真實可利用路徑，則直接作為漏洞證據輸出，附帶完整的攻擊路徑復現，供審計專家確認並跟進修復。兩條路徑共同驅動閉環收斂，直至數學意義上確認目標屬性對所有可能輸入均成立。經該閉環機制驗證的關鍵路徑，構成整個合約安全體系中確定性最強的防線，將攻擊面壓縮至極窄的範圍。
3.2 增強AI基線檢查：面向開發者的持續風險提示服務
同時，Beosin 也將基於 Skill 知識庫的增強 AI 基線檢查作為一項獨立服務提供給客戶。與專注於發現高危漏洞的人工深度審計不同，這項服務的定位更接近一份面向開發團隊的代碼健康報告。AI 基線掃描會對合約代碼進行全量覆蓋，系統性地梳理出那些當前不會直接造成經濟損失，但在項目後續維護和迭代過程中需要開發者關注的潛在問題。例如：使用了過時的依賴庫、缺失關鍵事件聲明、不符合最佳實踐的狀態變量暴露方式，以及可以進一步優化的 Gas 使用模式等。這些問題在當前的業務邏輯下通常不會被攻擊者直接利用，但隨著協議功能擴展、代碼重構或外部依賴更新，其中部分問題有可能逐步演變為真正的安全隱患。三個層次各有側重、逐層遞進，共同構建起對 Web3 項目安全的完整保障體系。
