Verification ladder

"It compiles" and "it is secure" are different claims. The ladder makes the difference legible: five levels, each earned, so a project can state what it proves instead of what it hopes.

The five levels

Levels are cumulative. A level only counts when every level below it holds, so achieved is the highest rung with unbroken support underneath, and it is -1 when even L0 fails.

• L0 typed contract - nifra check passes: the frontend and backend cannot have silently diverged.
• L1 route assurance - every route is classified, and the enforcement a rule requires is actually installed.
• L2 capability lockfile - declared effects match a reviewed lockfile, so a route that starts writing to the database shows up in review.
• L3 route manifest - the committed trust artifact still matches the routes, evidence, effects, and response classification it was emitted from.
• L4 invariant-tested - contract-derived invariants ran against an isolated executor with nothing skipped.

Run it

# What does this project prove right now?
nifra levels

# Fail CI below a level the project already reached.
nifra levels --min 2

# The same report an agent reads over MCP (nifra_levels).
nifra levels --json

L0  typed contract        ok
L1  route assurance       ok
L2  capability lockfile   ok
L3  route manifest        FAIL  manifest drifted from routes: run `nifra manifest emit`
L4  invariant-tested      FAIL  no isolated invariant executor configured

achieved: 2

Every level that does not hold explains itself, so the output is a work list rather than a verdict. --min <n> is the CI floor: pin it to the level you have reached and the build fails when a change quietly costs you a rung.

Wiring the levels

L0 needs nothing. L1 through L4 hang off nifra.assurance.ts, and each one you configure is a level you can start claiming.

// nifra.assurance.ts
// doc-check: skip - policy rules and the isolated executor are app-specific
import { defineAssuranceConfig } from "@nifrajs/core/assurance"
import { backend } from "./backend"

export default defineAssuranceConfig({
  source: backend,
  policy: { rules: [/* ... */] },
  capabilities: { lockfile: "capabilities.lock.json", policy: { /* ... */ } },
  manifest: { path: "nifra.manifest.json" },
  invariants: {
    // L4 fuzzes the contract, so it needs an app you are willing to throw hostile
    // input at. Point this at an isolated instance, never a live one.
    executor: (request) => backend.fetch(request),
  },
})

L4 requires an explicit executor. Invariant runs send deliberately hostile input, so Nifra will not guess which app to point them at; a level that fuzzed your live server by default would be a footgun, and a skipped route is reported rather than passed over in silence.

An app that needs a session, real row ids or signed tokens passes them to the runner instead of rewriting requests inside the executor: witnesses, prepareRequest, isRejected, include and maxMutationsPerInput on invariants reach every L4 run, from nifra levels and the nifra_levels MCP tool alike. setup provisions a throwaway target only when L4 runs: it is called once, before the first L4 request, and its teardown always runs after the run, a failing one included. The example keeps its target in memory; a database or container belongs in your own setup.

// nifra.assurance.ts
// doc-check: skip - the backend and its seed data are app-specific
import { defineAssuranceConfig } from "@nifrajs/core/assurance"
import { createBackend } from "./backend"

export default defineAssuranceConfig({
  source: createBackend({ rows: new Map() }),
  policy: { rules: [/* ... */] },
  invariants: {
    // Called once, before the first L4 request - never when this file is imported, so
    // `nifra check` and `nifra assure` provision nothing.
    setup: async () => {
      const rows = new Map([["row_1", { id: "row_1", owner: "fixture" }]])
      const target = createBackend({ rows })
      return {
        executor: (request) => target.fetch(request),
        teardown: () => rows.clear(), // runs after a failing run too
      }
    },
    // Known-good inputs for schemas L4 cannot synthesize (an opaque validator, a real id).
    witnesses: { "PATCH /rows/:id": { params: { id: "row_1" }, body: { title: "ok" } } },
    // Attach what the app needs on every case: a session, a signed token.
    prepareRequest: (request) => {
      const headers = new Headers(request.headers)
      headers.set("cookie", "session=fixture")
      return new Request(request, { headers })
    },
  },
})

Response contracts

Next to the ladder, nifra levels counts the routes that declare a response or errors schema and how each is held at runtime: enforced, warn-only (checked, original payload still sent) or typed-only (no responseContract() covers it). A typed-only route is usually registered on a server other than the one the plugin is installed on, or before it; the report names the routes and says which.

The count does not fail a level on its own. To make L1 require enforcement, add a baseline rule selecting hasResponse: true: unlike rules, where the first match owns a route, a baseline rule is checked on every route it matches, so one entry covers every class. A new app from create-nifra ships this baseline in its nifra.assurance.ts, beside the responseContract("enforce") its backend installs. nifra assure --strict also fails while any declared route is typed-only or warn-only.

// nifra.assurance.ts
// doc-check: skip - the backend is app-specific
import { defineAssuranceConfig, NIFRA_ASSURANCE } from "@nifrajs/core/assurance"
import { backend } from "./backend"

export default defineAssuranceConfig({
  source: backend,
  policy: {
    rules: [/* first match owns each route: classify by path, method, capability ... */],
    // Checked on every route it matches, whichever rule owns the route.
    baseline: [
      {
        name: "response-contract",
        match: { hasResponse: true },
        require: [NIFRA_ASSURANCE.RESPONSE_CONTRACT],
      },
    ],
  },
})

For coding agents

The nifra_levels MCP tool returns the same { achieved, levels[] } report. An agent can read what its change proved, and a level that regressed comes back with the reason it broke.