從規格、證據到證明：frama-c-mcp 白話指南

資訊查核日期：2026-09-14
適用範圍：frama-c-mcp 目前的實作，以及 C、C++、Rust、Go、Python 採用同類驗證流程的可行性。

先講結論

frama-c-mcp 是一個給 AI 代理程式使用的 C 程式正式驗證介面。「正式驗證」是把程式與 數學化規格轉成邏輯問題，再由分析器或證明器檢查，而不只是執行幾組測試資料。它把 Frama-C 的下列能力包裝成 MCP 工具：

• ACSL：寫在 C 程式旁的規格語言，用來描述呼叫條件、預期結果與可修改範圍。
• annotation（註記）：用 ACSL 寫下的規格，例如 requires、ensures 與迴圈不變量。
• EVA：以抽象解譯推估變數可能值與執行期錯誤，不必列舉每一個輸入。
• WP：把程式與 ACSL 規格轉成必須證明的邏輯命題，再交給證明器處理。
• E-ACSL：把可執行的 ACSL 規格轉成執行期檢查，實際執行程式以尋找違規案例。
• MCP：讓 AI 模型以統一協定呼叫外部工具與取得結構化結果的通訊協定。

因此，Claude、Codex 或其他 MCP 用戶端可以反覆執行：

讀程式 → 寫／讀規格 → 分析風險 → 產生證明義務 → 嘗試證明
       ↑                                           ↓
       └──────── 根據未證明原因修正程式或輔助規格 ────────┘

它不是新的 theorem prover，也不會自動知道產品需求。真正解析與驗證 C 的是 Frama-C，Alt-Ergo、Z3、CVC5 等 solver 負責嘗試解開 WP 產生的邏輯命題；本專案負責 AI-friendly 的操作、狀態管理、隔離實驗、完整性判斷與 proof receipt。

一句最精確的描述是：

在指定原始碼、build configuration、machine model、ACSL specification、分析設定與 明列 assumptions 下，蒐集 Frama-C evidence，並判斷要求的 proof obligations 是否 全部成立且沒有未交代缺口。

閱讀前的特殊用詞速查

以下用詞會在後文反覆出現。英文會保留，是因為工具輸出、設定名稱與錯誤訊息通常使用 原文；中文解釋則用來說明它在本文扮演的角色。

為什麼需要這個專案

一般 AI code review 很擅長指出「這裡看起來可能越界」，但這只是合理推測。即使 AI 說 「看起來沒問題」，也沒有列出它究竟考慮了哪些輸入、路徑或假設。

Frama-C 有更嚴謹的分析能力，但它的專案狀態、AST、annotations、WP goals、prover configuration 與結果不適合讓 agent 只靠零散 shell commands 操作。frama-c-mcp 在 兩者之間補上可反覆呼叫、可追蹤、失敗時能繼續調查的協定層。

系統架構

flowchart LR
    U[使用者<br/>需求與信任邊界] --> A[AI agent<br/>Claude / Codex / MCP client]
    A <-->|MCP JSON-RPC<br/>stdio| M[frama-c-mcp<br/>Rust server]

    subgraph S[frama-c-mcp session]
      M --> ST[專案狀態<br/>conclusions / receipts / lock]
      M --> R[tool router<br/>check / context / run_wp / ...]
    end

    R <-->|Unix socket<br/>Frama-C Server protocol| F[Frama-C main process]
    F <--> P[ast-utils plugin<br/>AST / ACSL / extraction / VC details]
    F --> EVA[EVA<br/>abstract interpretation]
    F --> WP[WP<br/>weakest precondition]
    WP --> SMT[Alt-Ergo / Z3 / CVC5<br/>或互動式 prover]

    R --> SB[Sandbox registry]
    SB --> X1[獨立 Frama-C process<br/>experiment:function]
    X1 <--> P1[ast-utils plugin]
    X1 --> SMT

    R --> E[E-ACSL<br/>instrument + compile + execute]
    M --> OUT[證據與結論<br/>缺口清單與證明收據]
    OUT --> A

每一層負責什麼

詳細模組邊界與可靠的代理程式呼叫順序，應以 frama-c-mcp 專案內的 architecture.md 與 agent-playbook.md 為準。

Specification、Evidence、Proof 到底差在哪裡

規格（Specification）：要守的約定

Specification 描述「程式應該做到什麼」，而不是重述每一行怎麼做。C 路線使用 ACSL：

propose_annotations 可以從 AST 抄出部分 frame facts，例如 loop 寫了哪些 locations。 但「加總的數學定義」「排序後保持 permutation」「權限檢查的產品政策」並不完整存在於 程式語法中，仍需人或 agent 撰寫並由 reviewer 確認。

證據（Evidence）：工具實際看見什麼

Evidence 是可供判斷的分析資料，不必然代表成功：

• source position 對應的 AST marker；
• EVA 的 before/after value sets 與 runtime alarms；
• WP 產生的 goal、status、prover、cache 狀態；
• 未證明 VC 的 hypotheses、separator 與 conclusion；
• caller/callee contracts、assumed dependencies；
• parser diagnostics、timeout、unmodeled header；
• E-ACSL 執行時的具體 counterexample；
• 本次驗證的 proof receipt。

好 evidence 必須能回答：「哪個檔案、哪個函式、哪一個 goal、在什麼環境、依賴哪些 假設，得到什麼結果？」只有一句「solver passed」是不夠的。

證明（Proof）：所有要求的義務都成立

WP 使用 weakest-precondition calculus，把 specification 倒推成執行前必須成立的邏輯 公式。外部 prover 再判斷這些 formulas 是否有效。

例如要證明 ensures \result >= 0，WP 不是執行幾個測資，而是根據每條控制流程推導：

對所有滿足 requires 的輸入 n，
如果 C 運算、memory model 與列出的 assumptions 成立，
則每一條會正常回傳的路徑都滿足 result >= 0。

本專案只有在要求的分析完成、goals 有效，而且 incomplete[] 為空時，才把整體 verdict 稱為 proved。這就是 fail-closed：沒跑、沒看完、timeout 或倚賴未證明假設，都不能 被「沒有報錯」包裝成成功。

證明收據（Proof receipt）：這份證明針對哪個執行環境

每次 check／run_wp 的 receipt 會綁定：

• 每個 source file 的 SHA-256 與整體 source_hash；
• 正規化 AST 的 ast_digest；
• include paths、system include paths、defines、forced includes、machdep；
• function scope 與 contracts；
• 有效 EVA/WP configuration；
• prover environment 與 per-goal statuses；
• incomplete[] 的 count、codes 與 digest；
• 整份內容的 SHA-256。

所以「同一份 C 文字但 -DNDEBUG 不同」仍是不同驗證條件；source 或 AST 改變，也不能 拿舊 receipt 冒充現在的證據。實作入口位於 frama-c-mcp 專案內的 src/mcp/receipt.rs。

receipt 是可重算、可比較的驗證紀錄，不是第三方數位簽章，也不是 Coq/Rocq kernel 可 獨立重播的 proof term。它證明「這個 session 回報過哪些 evidence」，不憑空提高底層 solver 或 memory model 的可信度。

完整驗證流程

flowchart TD
    A[取得真正 sources 與 build configuration] --> B[reload_project<br/>載入並建立 AST]
    B --> C{parse / plugin / environment<br/>是否完整？}
    C -- 否 --> C1[回報 incomplete 與 diagnostic<br/>不可假裝已驗證]
    C -- 是 --> D[讀 contract / call graph / AST context]
    D --> E{已有可信 contract？}
    E -- 否 --> F[propose_annotations<br/>先取得 code-determined frames]
    F --> G[人類或 agent 補 predicates<br/>requires / ensures / invariant]
    E -- 是 --> H[保留原始 requires / ensures]
    G --> I[dry-run ACSL validation]
    H --> I
    I -- 語法或型別失敗 --> G
    I -- 合法 --> J[create_sandbox<br/>抽取函式與依賴到獨立 process]
    J --> K[inject annotations]
    K --> L[EVA + WP]
    L --> M{所有 goals valid？}
    M -- 否 --> N[get_wp_goals<br/>alarm / investigation / VC]
    N --> O{原因}
    O -->|規格缺少輔助事實| G
    O -->|程式 bug| P[修改程式後重新載入]
    O -->|timeout/backend| Q[調整 prover 或拆 lemma]
    P --> B
    Q --> L
    M -- 是 --> R[合併已驗證 annotations 到 main]
    R --> S[main project 重新 run_wp/check]
    S --> T{缺口清單是否為空？}
    T -- 否 --> N
    T -- 是 --> U[verdict: proved<br/>產生 proof receipt]
    U --> V[store_function_conclusion<br/>供 bottom-up caller 驗證]

為什麼要 sandbox

錯誤 invariant 可能讓 WP 卡住，也可能污染同一個 Frama-C process 的 state。sandbox 會把 目標函式、型別、globals 與 callee dependencies 抽成暫存 C 檔，啟動獨立 Frama-C process。實驗失敗即可刪除重建；成功後再明確 merge 回 main，最後仍需在完整 project 重新證明。

為什麼要 bottom-up

caller 通常使用 callee contract，而不是展開 callee body。若 callee 尚未證明，caller 的綠色結果可能建立在「先相信 callee」上。因此 verify_program_step 依 call graph 讓 callee 優先，保存 conclusion，再驗證 caller；遞迴 strongly connected component 則需 當成群組處理。

一個具體 C／ACSL 範例

以下函式計算前 n 個非負整數的總和。為了讓範例集中在 proof structure，先排除 machine integer overflow；實務上還要補足能保證總和不超過 INT_MAX 的 bound。

/*@
  requires n >= 0;
  requires \valid_read(a + (0 .. n - 1));
  requires \forall integer k; 0 <= k < n ==> a[k] >= 0;
  assigns \nothing;
  ensures \result >= 0;
*/
int sum_nonnegative(const int *a, int n)
{
    int total = 0;

    /*@
      loop invariant 0 <= i <= n;
      loop invariant total >= 0;
      loop assigns i, total;
      loop variant n - i;
    */
    for (int i = 0; i < n; ++i)
        total += a[i];

    return total;
}

規格如何分工

1. n >= 0 排除負長度。
2. \valid_read(...) 保證每次 a[i] 都可讀。
3. quantified requires 保證每個元素非負。
4. assigns \nothing 表示不改動 caller 可觀察的 memory；local variables 不必列入 function frame。
5. ensures 是目標：回傳值非負。
6. 0 <= i <= n 把 array-bound fact 帶過 loop boundary。
7. total >= 0 把 postcondition 所需的中間事實帶到 loop exit。
8. n - i 用來證明終止。

WP 大致會產生哪些 obligations

Loop invariant initialization:
  requires  ==>  0 <= 0 <= n  且  total(0) >= 0

Loop invariant preservation:
  invariant 且 i < n 且 element assumptions
  ==> 執行 total += a[i], i++ 後 invariant 仍成立

Memory safety:
  0 <= i < n 且 valid_read(a[0 .. n-1])
  ==> a[i] 可讀

Loop variant:
  n - i >= 0，而且下一輪嚴格下降

Postcondition:
  invariant 且 !(i < n)
  ==> total >= 0

如果拿掉 total >= 0 invariant，函式直覺上仍然正確，但 WP 在 loop exit 未必保有足夠 關係推出 postcondition。這叫「缺少 proof hint」，不一定是程式 bug。

反過來，如果程式實際會 overflow，加入一條不真的成立的 invariant 也不能正當修復； 它自己的 initialization/preservation obligations 應該失敗。正確處理是限制 n／元素 大小、改用更寬型別，或改寫程式。

如何讀取成功、失敗與不完整

flowchart LR
    G[某個 WP goal] --> S{status}
    S -->|valid 且沒有異常依賴| P[局部 proof evidence]
    S -->|invalid / disproved| B[找到反例或規格衝突]
    S -->|unknown / timeout| U[尚未證明<br/>不等於為假]
    P --> C{所有要求的分析<br/>與 completeness checks}
    C -->|缺口清單為空| OK[整體 proved]
    C -->|有任何 gap code| NO[整體 incomplete]

常見阻擋項目：

完整的代碼詞彙位於 frama-c-mcp 專案內的 src/mcp/checkgaps.rs，ACSL 修正指引則見 該專案的 writing-acsl.md。

這套方法能不能用在其他語言

可以沿用「方法」，但不能直接沿用目前「實作」。這套方法需要五個可替換介面：

flowchart LR
    L[語言 front end<br/>parser / compiler IR] --> SP[Specification adapter]
    SP --> VE[Verification engine<br/>AI / VC generator / model checker]
    VE --> EV[Evidence normalizer<br/>goals / traces / assumptions]
    EV --> RC[Receipt + completeness policy]
    RC --> AG[Agent orchestration<br/>sandbox / retry / dependency order]

frama-c-mcp 現在的 front end、spec adapter 與 engine 都是 C-specific：Frama-C AST、 ACSL、EVA/WP、ast-utils requests。因此把 .rs、.go 或 .py 路徑交給現有 server 不會自動變成對應語言的 proof。要支援其他語言，應保留 orchestration、evidence schema、 fail-closed 與 receipt 思路，再為每種 verifier 實作 adapter。

C、C++、Rust、Go、Python 比較

C：最適合直接使用本專案

Frama-C 官方將 ACSL 定位為 C 的 formal behavioral specification language；WP 用 Hoare-style weakest preconditions 證明 ACSL properties，EVA 也可對 properties 與 runtime safety 提供分析結果。這正是本 repository 已實作的路徑。

適合：embedded、driver、parser、crypto primitives、memory-sensitive libraries，以及希望把 proof progress 接進 agent workflow／CI 的 C 專案。

C++：概念接近，但工程風險高於 C

Frama-C 生態有 Frama-Clang 與 ACSL++，所以在受控 C++ subset 上，可以建立很接近本文的 流程。然而官方 manual 列出的限制包含 C++ feature coverage、templates robustness、標準庫 specifications 與部分 ACSL++ constructs；不能因為底層仍是 Frama-C 就假定任意現代 C++ 專案可直接處理。

另一條路是 CBMC 類 bounded model checking。它對 C/C++ assertions、memory safety 與有限 loop unwind 很實用，並能給 counterexample trace。但結論 通常是「在這個 bound 與模型內找不到反例」，除非同時能證明 unwinding assertions／完整 涵蓋，否則不能改寫成 unbounded correctness proof。

建議：

• C-like、少 templates 的 C++ subset：評估 Frama-Clang/ACSL++。
• 需要快速找低階 bug、可設定明確 bounds：優先 CBMC/ESBMC adapter。
• 重度 templates、exceptions、coroutines、完整 STL：先做 capability probe，不能預設可驗證。

Rust：工具選擇最多，但保證類型不同

• Kani 是 bit-precise Rust model checker，使用 proof harnesses，擅長 panic、overflow、unsafe interaction 與 bounded state spaces。
• Creusot 把 annotated Rust 轉為 Why3 的中間驗證語言並產生 VCs， 很接近 ACSL/WP 的 deductive workflow。
• Verus 提供 specifications 與 proof language， 以 SMT 靜態驗證 executable Rust 對所有符合模型的執行滿足使用者規格。
• Prusti 基於 Viper，支援 contracts、 predicates 與 loop invariants；官方文件也明列預設及 partial-correctness 邊界。

Rust compiler 已提供 memory/type safety 的強大基線，但它不證明「排序真的排序」「餘額永不 變負」「協定狀態機符合需求」。這些仍需要 specifications 與對應 verifier。

若要做 Rust 版 MCP：Kani adapter 適合先做 counterexample-oriented MVP；Creusot 或 Verus adapter 更接近本專案的 specification/VC/proof/receipt 主軸。

Go：Gobra 最接近此專案的 deductive 路線

Gobra 是 Go 的 modular verifier，將 annotated Go 翻譯到 Viper，再用 SMT backend 驗證。官方 tutorial 描述的目標包含 memory safety、crash safety、data-race freedom，以及依使用者規格的 partial correctness。

它與此專案很容易建立概念映射：

困難在於 Go runtime、goroutines、channels、interfaces 與第三方 package specifications。Gobra 能處理並行推理不代表不寫 permissions/invariants 就會自動證明任意 production service。

Python：最適合先從「找反例」開始

CrossHair 會用帶有 Z3 expressions 的 symbolic objects 實際呼叫 Python functions，探索路徑，支援 assert、PEP 316、icontract 與 deal。它非常 適合以下 agent loop：

加入 contract → symbolic exploration → 回傳具體 counterexample
              → 修程式／contract → 重跑

但 Python 的動態行為與 native extensions 讓完整建模困難。CrossHair 自身也把定位描述為 介於 testing 與 type systems 的分析工具；timeout 或沒找到 counterexample，不能普遍解讀成 所有 Python executions 的 theorem。

Nagini 是基於 Viper 的 statically typed Python modular verifier，更接近 deductive verification，但適用 subset、annotations 與維護狀態都 需要在採用前做 capability probe。

建議 Python adapter 把結果分成：

• counterexample_found：強 evidence，帶具體輸入與 trace；
• bounded_or_timed_search_clear：指定 budget 內未找到；
• unsupported_semantics：native/side-effect/dynamic feature 未建模；
• deductively_verified：只能由明確具有此語意的 backend 產生。

不要把前兩者標成 proved。

跨語言共用的 MCP 架構建議

如果未來把這個專案擴充成多語言 verification MCP，建議不要把所有 backend 硬塞進相同 valid/invalid 字串。應共用外框、保留 backend semantics：

VerificationSubject
  language, files, source_hash, build_identity, target

SpecificationSet
  language, syntax, clauses, trusted_clauses, spec_hash

Obligation
  stable_id, owner, kind, source_span, formula?, dependencies

Evidence
  backend, backend_version, method
  status, assumptions, bounds, timeout, counterexample?, from_cache

Completeness
  requested_analyses, completed_analyses, unsupported_features, gaps[]

Receipt
  subject + specification + toolchain + obligations + completeness + sha256

其中 method 至少區分：

• abstract_interpretation
• deductive_verification
• bounded_model_checking
• symbolic_execution
• runtime_contract_checking
• proof_assistant_checked

同一個 status: valid 在不同 method 下不是相同承諾。receipt 必須帶 bounds、unwind completeness、unsupported features、trusted axioms、solver result 和 cache provenance。

建議的導入順序

只驗證 C

直接延伸目前專案：

1. 保存真實 compile database／preprocessor configuration。
2. 由安全性關鍵且依賴少的 leaf functions 開始。
3. 先建立 frame 與 runtime-safety specification。
4. 再加入 functional postconditions 與 loop invariants。
5. CI 使用 fail-closed verdict、goal floor 與 receipt freshness。
6. 對外部函式、axioms 與未證明 callee 建 trusted-base inventory。

多語言但先求實用

按「最容易得到有用 evidence」排序：

1. C：既有 Frama-C backend。
2. Rust：先接 Kani counterexamples，再視需求接 Creusot／Verus。
3. Python：CrossHair counterexample workflow，但禁止把 search-clear 寫成 proof。
4. Go：Gobra，適合願意投入 permissions/contracts 的關鍵 library。
5. C++：先限定受支援 subset；依需求選 Frama-Clang 或 bounded model checker。

多語言且要求一致 proof governance

先定義 backend-neutral receipt schema、completeness taxonomy 與 trust policy，再寫 adapters。 真正需要共用的是「不完整不能冒充成功」與「結論必須綁定 source/spec/toolchain」，不是要求 所有語言都回傳看似一致但語意不同的 proved。

這個專案證明了什麼、沒有證明什麼

能合理宣稱

• 對 receipt 指定的 source、AST、configuration 與 specification，列出的 WP obligations 得到了列出的 prover statuses。
• verdict: proved 且 incomplete[] 為空時，本 server 沒有發現其已知 completeness gaps。
• EVA alarms、VC hypotheses、counterexamples 與 dependency assumptions 可被 agent 進一步調查。
• receipt hash 能偵測內容差異並支援 session 內比較。

不能單靠它宣稱

• specification 等同真正產品需求；
• compiler、Frama-C、plugin、solver 或硬體完全沒有 bug；
• 未建模的 OS、I/O、assembly、foreign code 或 concurrency 行為正確；
• unknown／timeout 代表程式錯誤；
• 有限 runtime tests 沒失敗就代表所有輸入正確；
• bounded model checker 在某個 bound 沒找到反例就代表 unbounded proof；
• hash receipt 是第三方簽章或 independently checkable proof term；
• 現有 frama-c-mcp 可以直接分析 C++、Rust、Go 或 Python。

信任邊界

最後一個實務問題不是「proof 是不是數學」，而是「你相信哪一層」：

flowchart TB
    REQ[真實需求] --> SPEC[人工審查過的 specification]
    SPEC --> FRONT[語言 front end / semantics model]
    FRONT --> VC[VC generator / abstract domain]
    VC --> SOLVER[SMT solver / proof assistant]
    SOLVER --> SERVER[MCP evidence normalization]
    SERVER --> RECEIPT[receipt / CI policy]

自動 proof 最常見的失敗不是 solver 算錯，而是 specification 太弱、precondition 排除了真正 輸入、build identity 不符、callee／library models 被默認信任，或 analysis 根本沒完整跑完。 因此本專案最有價值的設計不只是「能呼叫 WP」，而是把 assumptions、incomplete[]、 source identity 與 proof receipt 一起帶回來。

參考資料

官方與原始資料

• Frama-C：ACSL
• Frama-C documentation
• Frama-Clang user manual
• CBMC
• Kani Rust Verifier
• Creusot
• Verus tutorial and reference
• Prusti user guide
• Gobra repository and tutorial
• Viper tutorial
• CrossHair documentation
• Nagini repository