保证案例

保证案例是团队关于系统足以胜任某一既定用途的论证：每一项主张、它所针对的用途，以及它所依据的证据。案例放在发布策略旁的 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 将其报告为团队的说法。

下一步

• 危险登记册 介绍目标可以依据的危险。
• 证据图 绘出每一项主张及其下方的证据。