# Verify Mode

Deterministic contract verification for CI and local development.

APOPHIS implements the invariant-driven approach from [Invariant-Driven Automated Testing](https://arxiv.org/abs/2602.23922) (Malhado Ribeiro, 2021): encode intended behavior as executable formulas, then verify them automatically with property-based generation and deterministic replay.

## When to Use It

- **Local development**: Quick feedback on behavioral changes
- **CI pipelines**: Catch regressions before merge
- **Pre-commit hooks**: Fast smoke verification

## Profile Examples

### Quick (local smoke)

```javascript
profiles: {
  quick: {
    name: 'quick',
    mode: 'verify',
    preset: 'safe-ci',
    routes: ['POST /users']
  }
}
```

### CI (PR checks)

```javascript
profiles: {
  ci: {
    name: 'ci',
    mode: 'verify',
    preset: 'safe-ci',
    routes: []
  }
}
```

Run with: `apophis verify --profile ci --changed`

### Deep (nightly verification)

```javascript
profiles: {
  deep: {
    name: 'deep',
    mode: 'verify',
    preset: 'safe-ci',
    routes: []
  }
}
```

## Route Filtering

Filter routes with the `--routes` flag:

```bash
# Single route
apophis verify --routes "POST /users"

# Multiple routes (comma-separated)
apophis verify --routes "POST /users,PUT /users/:id"

# Wildcards
apophis verify --routes "POST /users/*"

# All routes (empty or omitted)
apophis verify --profile quick
```

`*` and `?` wildcards are supported in `--routes`.

## `--changed` Flag

Run only routes modified in the current git branch:

```bash
apophis verify --profile ci --changed
```

If no routes changed, exits 2 with a message.

## Failure Output Format

When a contract fails, APOPHIS prints:

```text
Contract violation
POST /users
Profile: quick
Seed: 42

Expected
  response_code(GET /users/{response_body(this).id}) == 200

Observed
  GET /users/usr-123 returned 404

Why this matters
  The resource created by POST /users is not retrievable.

Replay
  apophis replay --artifact reports/apophis/failure-2026-04-28T12-30-22Z.json

Next
  Check the create/read consistency for POST /users and GET /users/{id}.
```

## Replay Workflow

1. Copy the replay command from failure output
2. Run it with the recorded route, seed, and artifact data; source or dependency drift can change the outcome
3. Fix the bug in your handler
4. Re-run verify to confirm the fix

```bash
apophis replay --artifact reports/apophis/failure-2026-04-28T12-30-22Z.json
```

Nondeterminism warnings appear in output when the same seed produces different results across runs. This indicates stateful behavior in your application that contracts cannot control.

## Machine Output for CI

Use concise formats to reduce log volume in large verify runs:

- `--format json-summary` — single JSON with summary, failures, warnings. Omits per-step traces.
- `--format ndjson-summary` — three NDJSON lines: `run.started`, `run.summary`, `run.completed`.

### Filtering examples

```bash
# Extract only failed routes from full ndjson
# Note: route.failed events are only emitted for failures, not passed routes
apophis verify --profile quick --format ndjson | jq 'select(.type == "route.failed")'

# Write artifact to disk and parse the file instead of stdout
apophis verify --profile quick --format json --artifact-dir reports/apophis
```

## Exit Codes

| Code | Meaning |
|---|---|
| 0 | All contracts passed |
| 1 | One or more behavioral contracts failed |
| 2 | Config error, no routes matched, no contracts found, or not a git repo |
| 3 | Internal APOPHIS error |
| 130 | Interrupted (SIGINT) |

## Config Example

```javascript
// apophis.config.js
export default {
  profile: 'quick',
  profiles: {
    quick: {
      mode: 'verify',
      preset: 'safe-ci',
      routes: ['POST /users']
    }
  },
  presets: {
    'safe-ci': {
      runs: 10,
      timeout: 5000
    }
  }
};
```

For the full config schema, see [CLI Reference](cli.md).

## Workspace Support

Run verify across all packages in a monorepo workspace:

```bash
apophis verify --workspace --profile quick --format json
```

Output includes per-package pass/fail summaries. Fails if any package fails.

## Test Budget

The `runs` field in your preset controls how many property-based tests execute per route. Default is 50. Lower for faster CI feedback, higher for deeper exploration:

```javascript
profiles: {
  quick: {
    mode: 'verify',
    preset: 'safe-ci',
    routes: ['POST /users']
  }
},
presets: {
  'safe-ci': {
    runs: 10,
    timeout: 5000
  }
}
```