Skip to content
Docs
ChangelogPricingOpen console

Guides

Assurance cases

An assurance case is your team's argument that a system is good enough for a stated use: each claim, the use it is made for, and the evidence it rests on. The case lives beside the release policy in assurance.yaml, so it is reviewed in pull requests, and Oloproof reads every claim against the evidence it holds. It never says a claim is proved: it says which claims rest on current passing evidence, which on failing, stale or missing evidence, and which on assumptions alone.

Writing the case

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]

A goal is a claim. A top-level goal states its scope, the intended use it is claimed for; a sub-goal inherits it. strategy says in words how the sub-goals argue the goal. Each piece of evidence names exactly one of:

  • rule: a rule of release.yaml, read at each system's latest run of each suite; system and suite narrow which runs count;
  • hazard: a hazard of hazards.yaml (Hazard register);
  • proof: a formal property, read as a proof rule reads it (Formal proofs): the last result received for the property, a DISPROVED of the same model winning; model (a digest) narrows it to one formalized model; until the project holds a result, the link supports nothing;
  • record: a decision record file written by oloproof record export, relative to the project root.

assumptions are what the goal takes for granted. A defeater is a reason the goal might be false; it stays open until every piece of its resolved_by evidence supports it. reassess_when says what should send the team back to the goal.

Checking it

oloproof assurance check

The check refuses a case that names a rule the policy does not hold or a hazard the register does not hold, or whose top-level goal states no scope, and exits 2. Otherwise it prints the tree, each goal with one of four statuses:

  • supported: every piece of its evidence and every sub-goal supports it, on current evidence, and no defeater is open;
  • undermined: some evidence fails, is stale or is contradicted, a sub-goal is undermined, or a defeater is open;
  • assumptions_only: nothing supports it, and it rests on stated assumptions;
  • unsupported: anything else, with each gap named. A goal with some support and a gap is unsupported: a claim is as strong as the weakest thing it rests on.

A rule supports a goal when every latest run that decided it says PASS, and undermines it when any says FAIL; INSUFFICIENT_EVIDENCE and MANUAL_REVIEW support nothing. A hazard supports when every rule that measures it passes. A formal result supports when the property was PROVED, and undermines when it was DISPROVED or when two results for one model disagree; a result says what it proves about the formalized model, never about the deployment. A record supports when its content still digests to its id and its decision is PASS. Evidence from a run that no longer matches the project (its system, suite, evaluators or policy changed) is stale and undermines. These statuses are the case's, never decisions, and they never change an exit code. --json writes the same report for a pipeline.

Where it shows

oloproof run records the case with the run, oloproof push carries the run's case to your workspace with the formal results its proof links name, and oloproof export writes the engine's reading of it beside the bundles. The Safety and risk page shows the tree with each status as the engine wrote it, each rule linked to its evidence. In the workspace the case is read against the runs you pushed: freshness is not compared there, because there is no project file to compare with, and record links are read only by oloproof assurance check. A decision record names the case its run recorded; record verify reports it as the team's word.

Where to go next