# Assurance levels

Five levels of proof that a change is right, from "it builds" to a machine-checked proof - what each checks, how to set them up, and what each still doesn't tell you.

"Done" from an agent is a claim. Assurance levels turn it into evidence. You choose how sure you need to be for each task or spec, Warden runs the checks, and every graded run is labelled with the highest level it reached and what that still doesn't prove.

## The five levels

| Level | Name | What Warden checks | What it still doesn't tell you |
|---|---|---|---|
| **L0** | Built | Your type-check, lint, build and existing tests pass. | Whether anything tests the new behaviour. |
| **L1** | Proven by a test | A test the agent added or changed **fails on the old code** and passes on the new. | Whether the test checks the edges. |
| **L2** | Non-trivially tested | Warden plants small bugs in the changed lines, one at a time, and your tests must catch at least half. | Whether it holds for inputs nobody wrote down. |
| **L3** | Lightweight formal | Property-based tests over many generated inputs pass. | Whether it holds for every input. |
| **L4** | Proof | A machine-checked proof (Dafny or Lean) against a spec you own. | Whether the spec says what you meant. |

Each level builds on the one below.

### How each level is checked

- **L1** finds the tests that are new or changed, and runs them twice: in a throwaway copy of your repository at the old code (they must fail) and in your working tree (they must pass). Supported for JavaScript and TypeScript, Python, PHP, Go, Java and Rust integration tests. If a faithful old copy can't be made, the result is *inconclusive*, never a pass.
- **L2** changes one changed line at a time (`true`↔`false`, `&&`↔`||`, `>=`→`>`, `==`→`!=` and similar), up to five such planted bugs in up to three files, and runs your tests against each. Your tests must be green first. Your files are always restored, and the bugs your tests missed are listed, so you know which line to test better.
- **L3** detects a property-testing framework in the changed tests (fast-check, Hypothesis, proptest, quickcheck, Go's testing/quick, rapid, jqwik, Eris) and runs those tests.
- **L4** needs a `.dfy` or `.lean` file in the change and runs `dafny verify` or `lake build`. Your own proof command can go in `.warden/formal.json`. No prover on your Mac? L4 isn't awarded, and Warden tells you so. It never fakes a proof.

## Use it

:::steps
1. **Set a level on a chat.** In the composer, **Set assurance**: *How hard should Warden work to be sure this change is right?* Each level shows whether this project is ready for it (git and a test runner for L1, and so on).
2. **Let it run.** Once a level is set, every turn that changes files runs the L0 checks and L1 in the background. The result appears in the chat, and when something fails in a way the agent can fix, the agent is told (at most three times in a row).
3. **Verify for the higher levels.** In the project's **Assurance** tab, **Verify changes** runs L1 to L4 against the restore point taken before the run, and records the level actually earned.
:::

**Run validations** in the composer runs everything (base checks, L1 to L4, your own gates) and hands the results to the agent. **Run independent grade** grades the change with your grader model.

## Set up your checks

**Assurance → Setup**:

- **Checks (L0)**: the commands that prove the project builds: `npm run lint`, `pnpm typecheck`, `pytest`. **Suggest from CI** reads them from your CI configuration; **Preview** runs them. Saved to `.warden/checks.json` in the repository, so the team shares them.
- **Your own gates at any level**: a command, a [workflow](workflows), a skill, *ask an agent*, or a **behaviour check** that drives your running app through its web UI, API or command line. Each gate is **Required** (a failure lowers the level earned) or advisory, and can apply to some languages only. A skill gate passes only when its reply ends with `WARDEN_GATE: PASS`.
- **Services**: `.warden/services.json` says how to start your app for behaviour checks; each worktree gets its own ports.

```json title=".warden/checks.json"
{
  "cwd": ".",
  "commands": [
    { "name": "Lint", "command": "pnpm lint" },
    { "name": "Types", "command": "pnpm typecheck" },
    { "name": "Tests", "command": "pnpm test" }
  ]
}
```

## Levels in your rules

The level a change has earned is a fact your rules can use:

```yaml
default: allow
rules:
  - deny: git push
    when: { trigger_mode: automated, assurance_meets_l2: "false" }
    reason: "Unattended pushes need L2"
```

The Software Factory sets a level per lane (L1 for Express and Standard, L2 for Assured) and can raise it per item. See [Lanes and gates](factory-lanes).

> [!LIMIT]
> L2 plants up to five bugs per change: a useful signal, not a full mutation-testing run. L4 needs Dafny or Lean installed. Your gates (other than `checks.json`) are stored on your Mac, not in the repository. Checks run inside the agent sandbox; one the sandbox blocks is marked *environment-limited*, with **Run outside the agent sandbox** after you confirm.