保證案例

保證案例是團隊關於系統足以勝任某一既定用途的論證：每一項主張、它所針對的用途，以及它所依據的證據。案例放在發布政策旁的 assurance.yaml 中，因此會在拉取請求中審查，Oloproof 會對照它所持有的證據讀取每一項主張。它從不說某項主張已被證明：它說明哪些主張依據目前通過的證據，哪些依據失敗、過時或缺少的證據，哪些僅依據假設。

撰寫案例

version: 1
goals:
  - id: G1
    statement: The assistant routes tickets well enough for first-line support
    scope: first-line support tickets in English
    strategy: argue over label accuracy and the misrouting hazard
    reassess_when: [the model changes, a new language is supported]
    goals:
      - id: G1.1
        statement: Labels are accurate
        evidence:
          - rule: label-floor
      - id: G1.2
        statement: Misrouting stays rare
        evidence:
          - hazard: missed-label
          - record: records/release-42.json
        defeaters:
          - id: D1
            statement: Tickets in other languages misroute
            resolved_by:
              - rule: label-floor
                suite: multilingual
      - id: G1.3
        statement: The deployment runs the model that was evaluated
        assumptions: [the model is pinned by digest in the deployment manifest]

目標就是一項主張。頂層目標陳述其 scope，即該主張所針對的預期用途；子目標繼承這個範圍。strategy 以文字說明子目標如何論證該目標。每一項 evidence 恰好指明下列一種：

• rule：release.yaml 中的一條規則，依每個系統在每個套件上的最新一次執行讀取；system 和 suite 限定計入哪些執行；
• hazard：hazards.yaml 中的一個危害（危害登記冊）；
• proof：一個形式化性質，依證明規則的方式讀取（形式化證明）：該性質最後收到的結果，同一模型的 DISPROVED 優先；model（一個摘要）將其限定為一個形式化模型；在專案持有結果之前，這條連結不支持任何東西；
• record：由 oloproof record export 寫出的決策紀錄檔案，路徑相對於專案根目錄。

assumptions 是目標視為理所當然的前提。defeater 是目標可能不成立的理由；在其 resolved_by 中的每一項證據都支持它之前，它一直處於未解決狀態。reassess_when 說明什麼情況應讓團隊重新審視該目標。

檢查

oloproof assurance check

檢查會拒絕列出政策中沒有的規則或登記冊中沒有的危害的案例，以及頂層目標未陳述範圍的案例，並以 2 結束。否則，它會印出目標樹，每個目標帶有下列四種狀態之一：

• supported：它的每一項證據和每一個子目標都支持它，依據的是目前的證據，且沒有未解決的反駁理由；
• undermined：某項證據失敗、過時或被反證，某個子目標被削弱，或存在未解決的反駁理由；
• assumptions_only：沒有任何東西支持它，它依據的是已陳述的假設；
• unsupported：其餘所有情況，並點名每一處缺口。有部分支持但存在缺口的目標即為不受支持：一項主張的強度取決於它所依據的最薄弱環節。

當判定了某條規則的每一次最新執行都給出 PASS 時，該規則支持目標；任何一次給出 FAIL 時，它削弱目標；INSUFFICIENT_EVIDENCE 和 MANUAL_REVIEW 不支持任何東西。當衡量某個危害的每條規則都通過時，該危害提供支持。形式化結果在性質為 PROVED 時提供支持，在性質為 DISPROVED 或同一模型的兩個結果不一致時削弱目標；結果說明的是它對形式化模型證明了什麼，從不涉及實際部署。當紀錄的內容仍能得出與其 id 一致的摘要且其決策為 PASS 時，紀錄提供支持。來自與專案不再相符的執行（其系統、套件、評估器或政策已變更）的證據是過時的，會削弱目標。這些狀態屬於案例，從來不是決策，也從不改變結束碼。--json 為流水線寫出同樣的報告。

顯示位置

oloproof run 隨執行記錄案例，oloproof push 把該執行的案例連同其證明連結所點名的形式化結果帶到你的工作區，oloproof export 把引擎對它的解讀寫在資料包旁邊。Safety and risk 頁面顯示這棵目標樹，每個狀態都與引擎寫出的一致，每條規則都連結到其證據。在工作區中，案例對照你推送的執行來讀取：那裡不比較新鮮度，因為沒有專案檔案可供比較，而紀錄連結只由 oloproof assurance check 讀取。決策紀錄會點名其執行所記錄的案例；record verify 將其回報為團隊的說法。

下一步

• 危害登記冊 介紹目標可以依據的危害。
• 證據圖 繪出每一項主張及其下方的證據。