---
title: Requirement traceability
description: "Generated by ./tools/check-trace.py --write; mise run trace:check fails when this file is stale, a requirement is in no file under verify/spec/traced/, or a traced requirement is…"
---

Generated by `./tools/check-trace.py --write`; `mise run trace:check` fails when
this file is stale, a requirement is in no file under `verify/spec/traced/`, or a
traced requirement is missing a layer. Requirements are defined in
`verify/spec/core.symspec.json` and `verify/spec/agentd.symspec.json`.

| Requirement | model | gherkin | fuzz | test | impl | live |
|---|---|---|---|---|---|---|
| AGENTD-1 | 1 | waived | waived | 2 | 1 | waived |
| AGENTD-2 | 1 | waived | waived | 2 | 1 | 1 |
| AGENTD-3 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-4 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-5 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-6 | 1 | waived | waived | 1 | 1 | 1 |
| AGENTD-7 | 1 | 1 | 1 | 4 | 4 | 1 |
| AGENTD-8 | 1 | 1 | 1 | 4 | 2 | 1 |
| AGENTD-9 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-10 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-11 | 1 | 1 | 1 | 4 | 3 | 1 |
| AGENTD-12 | 1 | 1 | 1 | 2 | 3 | 1 |
| AGENTD-13 | 1 | 1 | 1 | 3 | 1 | 1 |
| AGENTD-14 | 1 | 1 | 1 | 4 | 3 | 1 |
| AGENTD-15 | 1 | 1 | 1 | 2 | 2 | 1 |
| AGENTD-16 | 1 | 1 | 1 | 4 | 4 | 1 |
| AGENTD-17 | 1 | waived | 1 | 2 | 1 | waived |
| AGENTD-18 | 1 | waived | waived | 3 | 1 | 1 |
| AGENTD-19 | 1 | waived | waived | 1 | 1 | waived |
| AGENTD-20 | 1 | waived | 1 | 3 | 1 | waived |
| AGENTD-21 | 1 | waived | 1 | 1 | 1 | waived |
| AGENTD-22 | 1 | 1 | 1 | 4 | 3 | 2 |
| AGENTD-23 | 1 | 1 | 1 | 2 | 2 | 2 |
| AGENTD-24 | 1 | 1 | 1 | 2 | 1 | 1 |
| AGENTD-25 | waived | waived | waived | 2 | 1 | 1 |
| AGENTD-26 | waived | waived | waived | 1 | 1 | 1 |
| ARCH-1 | waived | waived | waived | 1 | 2 | waived |
| ARCH-2 | waived | waived | waived | 1 | 4 | waived |
| ARCH-3 | waived | waived | waived | 1 | 1 | waived |
| ARCH-4 | waived | waived | waived | 1 | 1 | waived |
| ARCH-5 | waived | waived | waived | 1 | 1 | waived |
| ARCH-6 | waived | waived | waived | 1 | 6 | waived |
| ARCH-7 | waived | waived | waived | 2 | 4 | waived |
| ARCH-8 | waived | waived | waived | 1 | 1 | waived |
| BIND-1 | waived | waived | waived | 1 | 2 | waived |
| BIND-2 | waived | waived | waived | 3 | 7 | waived |
| BIND-3 | waived | waived | waived | 1 | 1 | 1 |
| BIND-4 | waived | waived | waived | 1 | 1 | 1 |
| BIND-5 | waived | waived | waived | 2 | 2 | waived |
| BIND-6 | 1 | 1 | 1 | 5 | 7 | 1 |
| BIND-7 | 1 | 1 | 1 | 4 | 4 | 1 |
| BIND-8 | 1 | 1 | 1 | 4 | 2 | 1 |
| BIND-9 | 1 | 1 | 1 | 4 | 2 | 1 |
| BIND-10 | 1 | 1 | 1 | 5 | 6 | 1 |
| BIND-11 | 1 | 1 | 1 | 4 | 1 | 1 |
| BIND-12 | 1 | 1 | 1 | 5 | 3 | 1 |
| BIND-13 | 1 | 1 | 1 | 4 | 3 | waived |
| BIND-14 | waived | 1 | 1 | 3 | 3 | waived |
| BIND-15 | 1 | 1 | waived | 6 | 6 | 1 |
| BIND-16 | 1 | 1 | waived | 5 | 5 | 1 |
| BIND-17 | 1 | 1 | 1 | 2 | 4 | 1 |
| BIND-18 | 1 | 1 | 1 | 6 | 3 | 1 |
| BIND-19 | 1 | 1 | 1 | 3 | 1 | 1 |
| BIND-20 | 1 | 1 | 1 | 6 | 4 | 1 |
| BIND-21 | 1 | waived | 1 | 1 | 1 | 1 |
| BIND-22 | waived | waived | 1 | 1 | 1 | waived |
| BIND-23 | 1 | waived | 1 | 2 | 1 | 1 |
| BIND-24 | 1 | waived | 1 | 1 | 1 | waived |
| BIND-25 | waived | waived | waived | 1 | 1 | waived |
| BIND-26 | waived | waived | waived | 1 | 1 | waived |
| BIND-27 | waived | waived | waived | 1 | 1 | waived |
| CLI-1 | waived | waived | waived | 1 | 2 | waived |
| CLI-2 | waived | waived | waived | 1 | 5 | waived |
| CLI-3 | waived | waived | waived | 2 | 1 | 2 |
| CLI-4 | waived | waived | waived | 3 | 5 | 2 |
| CLI-5 | waived | waived | waived | 4 | 4 | waived |
| CLI-6 | waived | waived | waived | 5 | 6 | waived |
| CLI-7 | 1 | 1 | 1 | 3 | 8 | 1 |
| CLI-8 | 1 | 1 | 1 | 2 | 3 | 2 |
| CLI-9 | 1 | 1 | 1 | 2 | 3 | 1 |
| COST-1 | waived | waived | waived | 1 | 3 | 1 |
| COST-2 | waived | waived | waived | 2 | 3 | waived |
| COST-3 | waived | waived | waived | 1 | 3 | 1 |
| COST-4 | waived | waived | waived | 3 | 5 | 1 |
| COST-5 | waived | waived | waived | 3 | 2 | waived |
| COST-6 | waived | waived | waived | 1 | 1 | waived |
| COST-7 | waived | waived | waived | 1 | 1 | waived |
| COST-8 | waived | waived | waived | 1 | 1 | waived |
| COST-9 | waived | waived | waived | 3 | 4 | waived |
| COST-10 | waived | waived | waived | 4 | 3 | 1 |
| IMAGE-1 | 1 | 1 | 1 | 2 | 1 | waived |
| IMAGE-2 | 1 | 1 | 1 | 2 | 2 | 2 |
| IMAGE-3 | 1 | 1 | 1 | 2 | 2 | waived |
| IMAGE-4 | 1 | 1 | 1 | 1 | 2 | 1 |
| IMAGE-5 | waived | waived | waived | 2 | 2 | waived |
| IMAGE-6 | waived | 1 | 1 | 2 | 2 | 1 |
| IMAGE-7 | waived | 1 | 1 | 3 | 5 | 1 |
| IMAGE-8 | 1 | 1 | 1 | 2 | 4 | 1 |
| IMAGE-9 | 1 | 1 | waived | 2 | 1 | 1 |
| IMAGE-10 | 1 | 1 | waived | 2 | 1 | 1 |
| IMAGE-11 | 1 | 1 | waived | 1 | 1 | 1 |
| IMAGE-12 | waived | waived | waived | 2 | 2 | waived |
| STATE-1 | 1 | waived | waived | 2 | 3 | waived |
| STATE-2 | 1 | waived | waived | 2 | 4 | waived |
| STATE-3 | 1 | waived | waived | 2 | 3 | waived |
| STATE-4 | 1 | waived | waived | 2 | 1 | waived |
| STATE-5 | 1 | waived | waived | 2 | 6 | waived |
| STATE-6 | 1 | waived | waived | 2 | 1 | 1 |
| STATE-7 | 1 | waived | waived | 2 | 5 | 1 |
| STATE-8 | 1 | waived | waived | 5 | 5 | waived |
| STATE-9 | 1 | waived | waived | 2 | 1 | waived |
| STATE-10 | 1 | waived | waived | 2 | 1 | 1 |
| STATE-11 | 1 | waived | waived | 2 | 3 | waived |
| STATE-12 | 1 | waived | waived | 4 | 6 | 2 |
| TRAP-1 | waived | waived | waived | 9 | 19 | waived |
| TRAP-2 | waived | waived | waived | 1 | 5 | waived |
| TRAP-3 | waived | waived | waived | 1 | 6 | 1 |
| TRAP-4 | waived | 1 | 1 | 2 | 4 | waived |
| TRAP-5 | waived | waived | waived | 2 | 6 | waived |
| TRAP-6 | waived | 1 | waived | 3 | 11 | waived |
| TRAP-7 | waived | waived | waived | 5 | 7 | 1 |
| TRAP-8 | waived | waived | waived | 3 | 7 | waived |
| TRAP-9 | waived | waived | waived | 5 | 10 | waived |
| TRAP-10 | waived | waived | waived | 5 | 7 | waived |
| TRAP-11 | waived | waived | waived | 2 | 6 | waived |
| TRAP-12 | waived | waived | waived | 1 | 6 | waived |
| TRAP-13 | waived | waived | waived | 1 | 3 | 1 |

## AGENTD-1

While the agent token is not installed, the agentd shall reject the control request.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/tests/model_conformance.rs`, `crates/agentd/tests/turmoil_transport.rs`
* **impl:** `crates/agentd/src/auth.rs`
* **live:** waived: the platform runs the hook before it forwards any traffic (AGENTD-2's live check), so a live run never reaches the daemon before bootstrap

## AGENTD-2

When a bootstrap request presents a token and the agent token is not installed, the agentd shall install the agent token.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/src/state.rs`, `crates/agentd/tests/turmoil_transport.rs`
* **impl:** `crates/agentd/src/state.rs`
* **live:** `conformance/lanes/lifecycle.py`

## AGENTD-3

When a bootstrap request presents a token that differs from the installed agent token, the agentd shall reject the bootstrap request.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/src/state.rs`
* **impl:** `crates/agentd/src/state.rs`
* **live:** `conformance/lanes/bootstrap.py`

## AGENTD-4

When a bootstrap request presents a token equal to the installed agent token, the agentd shall accept the bootstrap request.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/src/state.rs`
* **impl:** `crates/agentd/src/state.rs`
* **live:** `conformance/lanes/bootstrap.py`

## AGENTD-5

When a control request presents a token that differs from the installed agent token, the agentd shall reject the control request.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/tests/turmoil_transport.rs`
* **impl:** `crates/agentd/src/auth.rs`
* **live:** `conformance/lanes/bootstrap.py`

## AGENTD-6

When a control request presents a token equal to the installed agent token, the agentd shall accept the control request.

* **model:** `crates/model/src/lib.rs`
* **gherkin:** waived: the token rules turn on two facts, whether a token is installed and whether the presented one equals it; the model checks every interleaving of them and the replay drives each against the daemon's routes, which a scenario would restate
* **fuzz:** waived: the verdict depends only on those two facts, which the model enumerates exhaustively, so there is no input space left for a fuzzer
* **test:** `crates/agentd/tests/turmoil_transport.rs`
* **impl:** `crates/agentd/src/auth.rs`
* **live:** `conformance/lanes/bootstrap.py`

## AGENTD-7

When a start request names its user or its group with a JSON string, the agentd shall resolve the name against the guest's /etc/passwd or /etc/group before it spawns the child.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/session.rs`, `crates/agentd/src/exec_start.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-8

If a start request names a user or a group that the guest's /etc/passwd or /etc/group does not contain, then the agentd shall answer Bad Request with the unknown\_user or unknown\_group error naming the value and spawn no child.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-9

When the user of a start request resolves to a passwd row, the agentd shall set HOME, USER and LOGNAME from the passwd row beneath the launch environment and the request environment.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-10

While a start request leaves inherit\_image\_env unset, the agentd shall build the child environment from the passwd identity, the launch environment and the request environment only.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-11

When a start request sets inherit\_image\_env, the agentd shall place the environment the agentd inherited at startup beneath the passwd identity, the launch environment and the request environment.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `crates/agentd/src/exec_start.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-12

The agentd shall exclude each AGENTD\_ variable and the agent token from the image environment snapshot.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec_start.rs`, `crates/agentd/src/lib.rs`, `crates/agentd/src/main.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-13

The agentd shall report on /v1/health whether an image environment snapshot exists and its key count, without its values.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/protocol/src/health.rs`
* **impl:** `crates/agentd/src/routes.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-14

When a start request names a shell, the agentd shall resolve the shell name on the child PATH, the image PATH, /bin and /usr/bin and run the command as the -c script of the resolved shell.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `bindings/microvms-py/src/session.rs`, `crates/agentd/src/exec_start.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-15

If a start request names a shell that no searched directory holds as an executable file, then the agentd shall answer Bad Request with the unknown\_shell error naming the shell and spawn no child.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-16

When a start request carries its user and group as integers and its shell as a boolean, the agentd shall demote the child to exactly those ids and run a true shell as /bin/sh -c.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/exec_start.mjs`, `bindings/microvms-py/tests/test_exec_start.py`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/session.rs`, `crates/agentd/src/exec_start.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** `conformance/lanes/exec.py`

## AGENTD-17

If the handshake of an identity-verified tunnel is not made with the host key the run hook pinned, then the agentd shall close the tunnel with close code 4403.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/agentd/src/tunnel_fuzz.rs`
* **test:** `crates/agentd/src/tunnel_identity.rs`, `crates/agentd/tests/tunnel_relay.rs`
* **impl:** `crates/agentd/src/tunnel_identity.rs`
* **live:** waived: no live check presents another host key: that needs a second host identity for one VM, and the relay tests drive the daemon's real route with one

## AGENTD-18

While the handshake of an identity-verified tunnel has not completed, the agentd shall not dial the guest port or relay any byte between the caller and the guest.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** waived: when the daemon dials is an order of steps, not a function of bytes; the tunnel model checks it over every interleaving and the relay tests against the daemon's real route
* **test:** `crates/agentd/tests/tunnel_relay.rs`, `crates/model-conformance/tests/tunnel_confirmation.rs`, `crates/model-conformance/tests/tunnel_end_of_stream.rs`
* **impl:** `crates/agentd/src/tunnel.rs`
* **live:** `conformance/lanes/tunnel.py`

## AGENTD-19

When the guest side of an identity-verified tunnel reaches the end of the guest stream, the agentd shall send the end of stream inside the Noise session before the agentd closes the tunnel.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** waived: what the daemon sends at a guest EOF doesn't depend on any byte it read; the tunnel model checks that the end precedes the close, and the client's frame harness that it opens only after every chunk
* **test:** `crates/agentd/tests/tunnel_relay.rs`
* **impl:** `crates/agentd/src/tunnel.rs`
* **live:** waived: the live suite's BIND-23 check observes it: the client reads Closed through the real proxy only when this end of stream crossed it

## AGENTD-20

If an identity-verified tunnel whose caller offered the end of stream ends without the caller's end of stream, then the agentd shall reset the guest connection rather than close the guest connection.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/agentd/src/tunnel_fuzz.rs`
* **test:** `crates/agentd/tests/tunnel_relay.rs`, `crates/microvms-edges/tests/tunnel_end_of_stream.rs`, `crates/model-conformance/tests/tunnel_end_of_stream.rs`
* **impl:** `crates/agentd/src/tunnel.rs`
* **live:** waived: a live run can't cut the endpoint proxy's connection mid-stream or withhold one frame, so no live check presents a caller end without its end of stream; the relay tests drive the daemon's real route

## AGENTD-21

If a frame of an identity-verified tunnel does not authenticate at the frame's position in the caller's stream, then the agentd shall end the tunnel without relaying the frame to the guest.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/agentd/src/tunnel_fuzz.rs`
* **test:** `crates/agentd/tests/tunnel_relay.rs`
* **impl:** `crates/agentd/src/tunnel.rs`
* **live:** waived: a live daemon and the endpoint proxy neither replay nor forge a frame, so a live run can't present one; the relay tests send both to the daemon's real route

## AGENTD-22

Where the image environment sets the default user, the agentd shall resolve the default user against the guest's /etc/passwd as the user of each start request that names no user.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/config.rs`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`, `crates/agentd/src/routes.rs`
* **impl:** `crates/agentd/src/config.rs`, `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/default_user.py`, `conformance/lanes/wrapped_user.py`

## AGENTD-23

Where the image environment sets the default user, the agentd shall demote the child of a start request that names its user to the named user rather than the default user.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/config.rs`, `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/default_user.py`, `conformance/lanes/wrapped_user.py`

## AGENTD-24

If a start request names no user and the guest's /etc/passwd does not contain the default user, then the agentd shall answer Bad Request with the unknown\_user error naming the default user setting and spawn no child.

* **model:** `crates/model/src/exec_start.rs`
* **gherkin:** `crates/agentd/tests/features/exec_start.feature`
* **fuzz:** `crates/agentd/src/exec_start_fuzz.rs`
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/exec_start.rs`
* **impl:** `crates/agentd/src/exec_start.rs`
* **live:** `conformance/lanes/default_user.py`

## AGENTD-25

When an accepted start request sets poweroff\_on\_exit to true, the agentd shall request guest power-off only after observing that the execution's original process group has no live members.

* **model:** waived: the process identities and liveness are Linux procfs observations; fixture snapshots and a real child group test the observer, while the live lane checks the guest shutdown path
* **gherkin:** waived: the route test starts a real shell and holds its background group member until after result publication; another textual scenario would restate that sequence
* **fuzz:** waived: the observer rejects malformed procfs records and tests PID reuse, disappearing entries, and zombie liveness directly; the shutdown action is injected so no fuzz input can power off the host
* **test:** `crates/agentd/src/exec.rs`, `crates/agentd/src/poweroff.rs`
* **impl:** `crates/agentd/src/poweroff.rs`
* **live:** `conformance/lanes/poweroff.py`

## AGENTD-26

When the image enables AGENTD\_DROP\_EXEC\_CAPABILITIES, the agentd shall verify that inheritable and ambient capabilities are empty and bounding capabilities SYS\_MODULE, SYS\_RAWIO, SYS\_PTRACE, SYS\_ADMIN, SYS\_BOOT, PERFMON, and BPF are absent while its permitted and effective capabilities remain unchanged before creating threads or serving requests.

* **model:** waived: the policy uses Linux thread capabilities; injected syscall failures and an isolated real capability subprocess test its state transitions
* **gherkin:** waived: the isolated subprocess exercises nonempty inheritable and ambient sets, thread creation, and exec directly; a textual scenario would repeat it
* **fuzz:** waived: strict boolean parsing and syscall postconditions are finite inputs exercised directly, and capability mutations belong only in isolated subprocesses
* **test:** `crates/agentd/src/exec_capabilities.rs`
* **impl:** `crates/agentd/src/exec_capabilities.rs`
* **live:** `conformance/lanes/capability_policy.py`

## ARCH-1

The microvms-core shall be the single library crate the CLI crate and the language bindings depend on, composing microvms-app with microvms-edges and re-exporting microvms-domain.

* **model:** waived: a property of the workspace's dependency graph, not of a state
* **gherkin:** waived: no behavior to script: cargo metadata's resolved graph is the evidence, and dependency\_direction.rs reads it
* **fuzz:** waived: there is no input stream; the rule is over manifests and re-exports
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-core/src/lib.rs`, `crates/microvms-domain/src/lib.rs`
* **live:** waived: composition makes no AWS call of its own

## ARCH-2

The microvms-core shall share protocol types with the agentd crate through a common dependency so that protocol drift fails compilation.

* **model:** waived: a property of the workspace's dependency graph, not of a state
* **gherkin:** waived: no behavior to script: the shared crate makes a wire-type mismatch a compile error, before anything runs
* **fuzz:** waived: there is no input stream; the rule is over manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/agentd/src/tunnel.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/protocol/src/identity.rs`, `crates/protocol/src/tunnel.rs`
* **live:** waived: a build-time property; the live tier runs a client and a daemon built from the one protocol crate, which is its premise, not a check of it

## ARCH-3

The CLI crate shall depend on microvms-core for each control-plane and endpoint-proxy operation.

* **model:** waived: a property of the workspace's dependency graph, not of a state
* **gherkin:** waived: no behavior to script: cargo metadata's resolved graph is the evidence, and dependency\_direction.rs reads it
* **fuzz:** waived: there is no input stream; the rule is over manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-cli/src/main.rs`
* **live:** waived: a dependency edge makes no AWS call

## ARCH-4

The microvms-core shall not depend on the CLI crate.

* **model:** waived: a property of the workspace's dependency graph, not of a state
* **gherkin:** waived: no behavior to script: cargo metadata's resolved graph is the evidence, and dependency\_direction.rs reads it
* **fuzz:** waived: there is no input stream; the rule is over manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-core/src/lib.rs`
* **live:** waived: a dependency edge makes no AWS call

## ARCH-5

The CLI crate shall not carry any type or function a language binding needs.

* **model:** waived: a property of the CLI crate's targets and of the capability table, not of a state
* **gherkin:** waived: no behavior to script: cargo metadata and the capability table are the evidence, and dependency\_direction.rs reads both
* **fuzz:** waived: there is no input stream; the rule is over the crate's targets and the table
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-cli/src/main.rs`
* **live:** waived: a crate's targets and the table's cells make no AWS call

## ARCH-6

The microvms-domain shall not perform network, filesystem, subprocess, environment, clock, or entropy access.

* **model:** waived: a property of a crate's code and dependencies, not of a state
* **gherkin:** waived: no behavior to script: clippy and the dependency set enforce it at build time
* **fuzz:** waived: there is no input stream; the rule is over source and manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-core/src/lib.rs`, `crates/microvms-core/src/prelude.rs`, `crates/microvms-domain/src/cost.rs`, `crates/microvms-domain/src/identity.rs`, `crates/microvms-domain/src/lib.rs`, `crates/microvms-domain/src/names.rs`
* **live:** waived: the domain makes no AWS call by construction

## ARCH-7

The microvms-app shall not depend directly on a crate or a tokio feature that performs network, AWS, filesystem, subprocess, or entropy I/O.

* **model:** waived: a property of a crate's code and dependencies, not of a state
* **gherkin:** waived: no behavior to script: clippy and the dependency set enforce it at build time
* **fuzz:** waived: there is no input stream; the rule is over source and manifests
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-app/src/lib.rs`, `crates/microvms-app/src/workspace.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-edges/src/lib.rs`
* **live:** waived: the app's AWS calls all go through ports, so the live tier exercises the edges' implementations, not this rule

## ARCH-8

The microvms-core shall not contain logic beyond composition and re-exports.

* **model:** waived: a property of a crate's code and dependencies, not of a state
* **gherkin:** waived: no behavior to script: the dependency set and the ratchet check it over source and manifests
* **fuzz:** waived: there is no input stream; the rule is over source and manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `crates/microvms-core/src/lib.rs`
* **live:** waived: composition makes no AWS call of its own

## BIND-1

The language bindings layer shall depend on microvms-core and, among the crates below it, only on microvms-protocol, with no dependency edge to the CLI crate.

* **model:** waived: a property of the workspace's dependency graph, not of a state
* **gherkin:** waived: no behavior to script: cargo metadata's resolved graph is the evidence, and dependency\_direction.rs reads it
* **fuzz:** waived: there is no input stream; the rule is over manifests
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `bindings/microvms-js/src/lib.rs`, `bindings/microvms-py/src/lib.rs`
* **live:** waived: a dependency edge makes no AWS call

## BIND-2

The language bindings layer shall not expose a parameter that bypasses a trap closure enforced in microvms-core.

* **model:** waived: a property of each binding's parameter surface, not of a state
* **gherkin:** waived: no Gherkin tier drives the bindings; their own suites call each surface and assert the refusal comes from core
* **fuzz:** waived: the surface is a fixed set of signatures, not an input stream; the closures it must not reopen live in core, whose tests and harnesses exercise them
* **test:** `bindings/microvms-py/tests/test_exec.py`, `bindings/microvms-py/tests/test_session.py`, `bindings/microvms-py/tests/test_smoke.py`
* **impl:** `bindings/microvms-js/src/errors.rs`, `bindings/microvms-js/src/exec.rs`, `bindings/microvms-js/src/hooks.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/exec.rs`, `bindings/microvms-py/src/hooks.rs`, `bindings/microvms-py/src/sandbox.rs`
* **live:** waived: the live suite drives the CLI, and a binding makes no AWS call core doesn't make; the closures it must not bypass are core's, checked offline

## BIND-3

The Python binding shall deposit a thin idiomatic wrapper over microvms-core via PyO3.

* **model:** waived: a property of the crate's dependencies and surface, not of a state
* **gherkin:** waived: no behavior to script: the dependency set and the adapter-logic ratchet check it over manifests and source
* **fuzz:** waived: there is no input stream; the rule is over manifests and source
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `bindings/microvms-py/src/lib.rs`
* **live:** `conformance/lanes/bindings.py`

## BIND-4

The JavaScript binding shall deposit a thin idiomatic wrapper over microvms-core via napi-rs.

* **model:** waived: a property of the crate's dependencies and surface, not of a state
* **gherkin:** waived: no behavior to script: the dependency set and the adapter-logic ratchet check it over manifests and source
* **fuzz:** waived: there is no input stream; the rule is over manifests and source
* **test:** `crates/microvms-cli/tests/dependency_direction.rs`
* **impl:** `bindings/microvms-js/src/lib.rs`
* **live:** `conformance/lanes/bindings.py`

## BIND-5

The language bindings layer shall preserve the cost honesty rules, exposing provenance-labelled durations, estimate-typed dollars, and the distinct Unpriced value.

* **model:** waived: a property of the bindings' cost types, which have no states to explore
* **gherkin:** waived: no behavior to script: each binding's suite asserts the shut doors directly, the coercions, the missing constructor and the absent usd key
* **fuzz:** waived: there is no input stream; the rule is over each binding's type surface, which the suites enumerate spelling by spelling
* **test:** `bindings/microvms-js/__test__/smoke.mjs`, `bindings/microvms-py/tests/test_smoke.py`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`
* **live:** waived: the bindings' cost types are local values and make no AWS call; the live suite holds core's report through the CLI (COST-1, COST-3, COST-4, COST-10)

## BIND-6

The microvms-core shall report a finished exec's POSIX exit code as 124 when a deadline ended the command, as 128 plus the signal number for any other signal death, and otherwise as the exit code.

* **model:** `crates/model/src/run.rs`
* **gherkin:** `crates/microvms-core/tests/features/run_to_completion.feature`
* **fuzz:** `crates/microvms-core/tests/run_to_completion_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/run_to_completion.mjs`, `bindings/microvms-py/tests/test_run_to_completion.py`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-core/tests/live_run_to_completion.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `bindings/microvms-js/src/exec.rs`, `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/exec.rs`, `bindings/microvms-py/src/session.rs`, `crates/microvms-app/src/session/complete.rs`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-cli/src/commands/attached.rs`
* **live:** `conformance/lanes/sessions.py`

## BIND-7

The microvms-core shall annotate an exec result with one human-readable note for each of truncated output, an expired daemon deadline, writers left alive past the linger deadline, an expired client deadline, and a synthesized result.

* **model:** `crates/model/src/run.rs`
* **gherkin:** `crates/microvms-core/tests/features/run_to_completion.feature`
* **fuzz:** `crates/microvms-core/tests/run_to_completion_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/run_to_completion.mjs`, `bindings/microvms-py/tests/test_run_to_completion.py`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-core/tests/live_run_to_completion.rs`
* **impl:** `bindings/microvms-js/src/exec.rs`, `bindings/microvms-py/src/exec.rs`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-cli/src/commands/attached.rs`
* **live:** `conformance/lanes/sessions.py`

## BIND-8

If the output stream of a run-to-completion call ends without the terminal exit event, then the microvms-core shall fall back to waiting for and acknowledging the exec and return exactly one result.

* **model:** `crates/model/src/run.rs`
* **gherkin:** `crates/microvms-core/tests/features/run_to_completion.feature`
* **fuzz:** `crates/microvms-core/tests/run_to_completion_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/run_to_completion.mjs`, `bindings/microvms-py/tests/test_run_to_completion.py`, `crates/microvms-app/src/session/complete.rs`, `crates/microvms-core/tests/live_run_to_completion.rs`
* **impl:** `crates/microvms-app/src/session/complete.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** `conformance/lanes/sessions.py`

## BIND-9

If the client deadline of a run-to-completion call expires before the exec's result is acknowledged, then the microvms-core shall signal the exec's process group before acknowledging the exec within the client grace period.

* **model:** `crates/model/src/run.rs`
* **gherkin:** `crates/microvms-core/tests/features/run_to_completion.feature`
* **fuzz:** `crates/microvms-core/tests/run_to_completion_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/run_to_completion.mjs`, `bindings/microvms-py/tests/test_run_to_completion.py`, `crates/microvms-app/src/session/complete.rs`, `crates/microvms-core/tests/live_run_to_completion.rs`
* **impl:** `crates/microvms-app/src/session/complete.rs`, `crates/microvms-app/src/session/exec.rs`
* **live:** `conformance/lanes/sessions.py`

## BIND-10

If the acknowledgement that follows a client-deadline kill fails, then the microvms-core shall return a synthesized result whose POSIX exit code is 124 and whose notes name the failure.

* **model:** `crates/model/src/run.rs`
* **gherkin:** `crates/microvms-core/tests/features/run_to_completion.feature`
* **fuzz:** `crates/microvms-core/tests/run_to_completion_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/run_to_completion.mjs`, `bindings/microvms-py/tests/test_run_to_completion.py`, `crates/microvms-app/src/session/complete.rs`, `crates/microvms-cli/src/guards/exec.rs`, `crates/microvms-core/tests/live_run_to_completion.rs`
* **impl:** `bindings/microvms-js/src/exec.rs`, `bindings/microvms-py/src/exec.rs`, `crates/microvms-app/src/session/complete.rs`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/commands/attached.rs`
* **live:** `conformance/lanes/sessions.py`

## BIND-11

The microvms-core shall derive a launch's egress posture from its launch options alone, as open when managed internet egress is requested, best-effort when the advisory deny is requested, and unsealed otherwise, and never as sealed.

* **model:** `crates/model/src/posture.rs`
* **gherkin:** `crates/microvms-core/tests/features/egress_posture.feature`
* **fuzz:** `crates/microvms-app/src/control/posture_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/egress_posture.mjs`, `bindings/microvms-py/tests/test_egress_posture.py`, `crates/microvms-app/src/control/connector.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/connector.rs`
* **live:** `conformance/lanes/posture.py`

## BIND-12

The language bindings layer shall expose on each session the egress posture the CLI envelope reports for the same launch options, and unsealed for a session whose launch options the session does not hold.

* **model:** `crates/model/src/posture.rs`
* **gherkin:** `crates/microvms-core/tests/features/egress_posture.feature`
* **fuzz:** `crates/microvms-app/src/control/posture_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/egress_posture.mjs`, `bindings/microvms-py/tests/test_egress_posture.py`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/guards/run.rs`, `crates/microvms-core/tests/live_posture.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`
* **live:** `conformance/lanes/posture.py`

## BIND-13

When a caller asks for the egress posture of a set of launch options, the microvms-core shall answer with the posture a launch with those options would report, or with the invalid-argument refusal the launch would raise, without any AWS call.

* **model:** `crates/model/src/posture.rs`
* **gherkin:** `crates/microvms-core/tests/features/egress_posture.feature`
* **fuzz:** `crates/microvms-app/src/control/posture_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/egress_posture.mjs`, `bindings/microvms-py/tests/test_egress_posture.py`, `crates/microvms-app/src/control/connector.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/connector.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`
* **live:** waived: a pure function that makes no AWS call; its refusals precede any call, so the service never sees them (zero calls asserted by the Gherkin scenarios and the fuzz harness)

## BIND-14

The sizing model shall select for a resource request the smallest size class whose baseline memory and baseline vCPU both cover the request, the default class when the request names neither, and an invalid-argument refusal naming the largest class when no class covers the request.

* **model:** waived: a stateless selection over the five-row size table; the bolero harness checks minimality and coverage over arbitrary requests instead
* **gherkin:** `crates/microvms-core/tests/features/request_and_preflight.feature`
* **fuzz:** `crates/microvms-domain/src/sizing_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/request_and_preflight.mjs`, `bindings/microvms-py/tests/test_request_and_preflight.py`, `crates/microvms-domain/src/sizing.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/sizing.rs`
* **live:** waived: a pure function of the request and the documented table; it makes no AWS call

## BIND-15

When a caller asks for a preflight, the microvms-core shall report whether the region resolves to a supported region, whether the credential chain resolves credentials, and whether the MicroVMs service answers a free read-only listing in that region, as one report whose ok is true only when every fatal check passed.

* **model:** `crates/model/src/preflight.rs`
* **gherkin:** `crates/microvms-core/tests/features/request_and_preflight.feature`
* **fuzz:** waived: the outcome space (3 region x 2 credential x 3 service worlds) is enumerated exhaustively by the Stateright model; there is no input stream to fuzz
* **test:** `bindings/microvms-js/__test__/request_and_preflight.mjs`, `bindings/microvms-py/tests/test_request_and_preflight.py`, `crates/microvms-app/src/preflight.rs`, `crates/microvms-cli/src/guards/doctor.rs`, `crates/microvms-core/tests/live_preflight.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `bindings/microvms-js/src/preflight.rs`, `bindings/microvms-py/src/preflight.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/transport.rs`, `crates/microvms-app/src/preflight.rs`, `crates/microvms-domain/src/preflight.rs`
* **live:** `conformance/lanes/local.py`

## BIND-16

The microvms-core shall not make a billable or mutating AWS call during a preflight, nor any AWS call after the region or the credentials failed to resolve.

* **model:** `crates/model/src/preflight.rs`
* **gherkin:** `crates/microvms-core/tests/features/request_and_preflight.feature`
* **fuzz:** waived: the outcome space (3 region x 2 credential x 3 service worlds) is enumerated exhaustively by the Stateright model; there is no input stream to fuzz
* **test:** `bindings/microvms-js/__test__/request_and_preflight.mjs`, `bindings/microvms-py/tests/test_request_and_preflight.py`, `crates/microvms-app/src/preflight.rs`, `crates/microvms-core/tests/live_preflight.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `bindings/microvms-js/src/preflight.rs`, `bindings/microvms-py/src/preflight.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/preflight.rs`, `crates/microvms-domain/src/preflight.rs`
* **live:** `conformance/lanes/local.py`

## BIND-17

When a caller requests the agentd daemon binary, the language bindings layer shall return the agentd binary that microvms-core resolves from a caller-supplied path, then the cache entry for the requested version, then the release asset for that version, with the version defaulting to the core version.

* **model:** `crates/model/src/provision.rs`
* **gherkin:** `crates/microvms-core/tests/features/provision.feature`
* **fuzz:** `crates/microvms-edges/src/provision_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/provision.mjs`, `crates/microvms-edges/src/provision.rs`
* **impl:** `bindings/microvms-js/src/provision.rs`, `bindings/microvms-py/src/provision.rs`, `crates/microvms-edges/src/lib.rs`, `crates/microvms-edges/src/provision.rs`
* **live:** `conformance/lanes/quickstart.py`

## BIND-18

If a fetched agentd release asset fails its attestation or SHA256SUMS verification, or neither verification can run, then the microvms-core shall fail with ERR\_PRECONDITION without returning or caching the bytes.

* **model:** `crates/model/src/provision.rs`
* **gherkin:** `crates/microvms-core/tests/features/provision.feature`
* **fuzz:** `crates/microvms-edges/src/provision_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/provision.mjs`, `crates/microvms-app/src/provision.rs`, `crates/microvms-edges/src/provision.rs`, `crates/microvms-edges/src/provision/release.rs`, `crates/microvms-edges/tests/provision_concurrent.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/provision.rs`, `crates/microvms-edges/src/provision.rs`, `crates/microvms-edges/src/provision/release.rs`
* **live:** `conformance/lanes/quickstart.py`

## BIND-19

If a cached agentd binary does not match the digest recorded when its release asset was verified, then the microvms-core shall discard the entry and fetch the release asset again.

* **model:** `crates/model/src/provision.rs`
* **gherkin:** `crates/microvms-core/tests/features/provision.feature`
* **fuzz:** `crates/microvms-edges/src/provision_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/provision.mjs`, `crates/microvms-edges/src/provision.rs`, `crates/microvms-edges/tests/provision_concurrent.rs`
* **impl:** `crates/microvms-edges/src/provision.rs`
* **live:** `conformance/lanes/quickstart.py`

## BIND-20

If a caller-supplied or fetched agentd binary is not an aarch64 ELF executable, then the microvms-core shall refuse it with ERR\_PRECONDITION.

* **model:** `crates/model/src/provision.rs`
* **gherkin:** `crates/microvms-core/tests/features/provision.feature`
* **fuzz:** `crates/microvms-edges/src/provision_fuzz.rs`
* **test:** `bindings/microvms-js/__test__/image_daemon.mjs`, `bindings/microvms-js/__test__/provision.mjs`, `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-cli/src/guards/build.rs`, `crates/microvms-edges/src/provision.rs`
* **impl:** `bindings/microvms-js/src/provision.rs`, `bindings/microvms-py/src/provision.rs`, `crates/microvms-domain/src/provision.rs`, `crates/microvms-edges/src/provision.rs`
* **live:** `conformance/lanes/quickstart.py`

## BIND-21

If the far end of an identity-verified tunnel does not complete the handshake against the VM public key pinned in the name record, then the microvms-core shall fail the tunnel rather than relay the local connection through the tunnel.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/microvms-edges/src/session/tunnel_fuzz.rs`
* **test:** `crates/microvms-core/tests/tunnel_end_to_end.rs`
* **impl:** `crates/microvms-edges/src/session/tunnel.rs`
* **live:** `conformance/lanes/tunnel.py`

## BIND-22

If a daemon event stream carries bytes that are not well-formed server-sent events, then the microvms-core shall drop the frame or end the stream with an error, without a panic and without holding more than 4 MiB of bytes that no frame terminator ends between reads.

* **model:** waived: one stream read by one parser has no interleavings to explore; its input space is bytes
* **gherkin:** waived: hostile bytes aren't a scenario a caller drives; the parser's tests feed it directly
* **fuzz:** `crates/microvms-app/src/session/sse_fuzz.rs`
* **test:** `crates/microvms-app/src/session/sse.rs`
* **impl:** `crates/microvms-app/src/session/sse.rs`
* **live:** waived: a live daemon sends well-formed events, so a live run can't present hostile bytes

## BIND-23

If the far end of an identity-verified tunnel whose daemon offered the end of stream closes the tunnel without the daemon's end of stream, then the microvms-core shall report the tunnel as truncated rather than closed.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/microvms-edges/src/session/tunnel_fuzz.rs`
* **test:** `crates/microvms-edges/tests/tunnel_end_of_stream.rs`, `crates/model-conformance/tests/tunnel_end_of_stream.rs`
* **impl:** `crates/microvms-edges/src/session/tunnel.rs`
* **live:** `conformance/lanes/tunnel.py`

## BIND-24

If a frame of an identity-verified tunnel does not authenticate at the frame's position in the daemon's stream, then the microvms-core shall fail the tunnel without writing the frame to the local connection.

* **model:** `crates/model/src/tunnel.rs`
* **gherkin:** waived: no Gherkin tier drives the tunnel: its tests speak the WebSocket and Noise wire themselves, which a scenario would only restate
* **fuzz:** `crates/microvms-edges/src/session/tunnel_fuzz.rs`
* **test:** `crates/microvms-edges/tests/tunnel_end_of_stream.rs`
* **impl:** `crates/microvms-edges/src/session/tunnel.rs`
* **live:** waived: a live daemon and the endpoint proxy neither replay nor forge a frame, so a live run can't present one; the stand-in tests send both to the client's real relay

## BIND-25

When a caller awaits the awaitable twin of a Python binding method that calls AWS or the daemon, the Python binding shall run the future that the method's blocking spelling runs, with the same arguments, as a task on the binding's shared runtime, and answer that future's result or its error class.

* **model:** waived: one future behind two spellings has no state of its own to explore; the future's states are core's, which its models hold
* **gherkin:** waived: no Gherkin tier drives the bindings; the Python suite calls each twin beside its blocking spelling and compares the answers
* **fuzz:** waived: the surface is a fixed set of signatures, not an input stream; the census test enumerates it twin by twin
* **test:** `bindings/microvms-py/tests/test_async.py`
* **impl:** `bindings/microvms-py/src/runtime.rs`
* **live:** waived: a twin makes the AWS calls its blocking spelling makes and no other; the live suite drives those through the CLI and core

## BIND-26

If a caller cancels the awaitable twin of a Python binding call that is not a lifecycle transition, then the Python binding shall abort the call's task at its next await.

* **model:** waived: cancellation is the runtime's abort of one task, not a protocol state; the core's own models hold the states a dropped request leaves
* **gherkin:** waived: no Gherkin tier drives the bindings; the Python suite cancels a twin against a loopback daemon and a stalling proxy
* **fuzz:** waived: there is no input stream; the rule is over which spawn a twin calls
* **test:** `bindings/microvms-py/tests/test_async.py`
* **impl:** `bindings/microvms-py/src/runtime.rs`
* **live:** waived: a cancelled read makes no AWS call a live run could observe that the loopback tests don't; the proxy test watches the connection itself

## BIND-27

If a caller cancels the awaitable twin of a lifecycle transition (a launch, a non-content-addressed image build, a suspend, a resume or a teardown), then the Python binding shall run the transition to completion on the object that started it.

* **model:** waived: cancellation is the runtime's choice not to abort one task; the transitions it lets finish are core's, which its models hold
* **gherkin:** waived: no Gherkin tier drives the bindings; the Python suite cancels a lifecycle twin through a stalling proxy
* **fuzz:** waived: there is no input stream; the rule is over which spawn a twin calls
* **test:** `bindings/microvms-py/tests/test_async.py`
* **impl:** `bindings/microvms-py/src/runtime.rs`
* **live:** waived: launching a VM to cancel its launch costs a billable VM per run for what the proxy test shows offline: the request stays open after the awaitable is gone

## CLI-1

The CLI crate shall render its interactive surface with ratatui.

* **model:** waived: a rendering choice, not a state
* **gherkin:** waived: the TUI draws only when stdout is a terminal, and the Gherkin tier runs the binary on pipes
* **fuzz:** waived: a frame is drawn from rows the command has already rendered as text; there is no input stream
* **test:** `crates/microvms-cli/src/tui.rs`
* **impl:** `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/src/tui.rs`
* **live:** waived: the live suite runs the CLI with --json on a pipe, where the TUI never draws

## CLI-2

The CLI crate shall reach the control plane and the endpoint proxy only through microvms-core.

* **model:** waived: a property of the crate's dependencies and of its one door to core, not of a state
* **gherkin:** waived: the behavioral guard already drives every AWS-touching command through a seam that refuses, which a scenario would restate
* **fuzz:** waived: there is no input stream; the rule is over the dependency set and the source
* **test:** `crates/microvms-cli/src/guards/thinness.rs`
* **impl:** `crates/microvms-app/src/session/exec.rs`, `crates/microvms-cli/src/commands/attached.rs`, `crates/microvms-cli/src/commands/local.rs`, `crates/microvms-cli/src/provision.rs`, `crates/microvms-cli/src/seam.rs`
* **live:** waived: a live run can't show that a call didn't bypass core; the dependency denylist, the clippy bans and the refusing seam can

## CLI-3

The CLI crate shall emit a stable exit code per documented failure class, distinct from the code for an unexpected error.

* **model:** waived: a fixed table from failure class to code, not a state machine
* **gherkin:** waived: the table-driven test asserts every row, and tests/exit\_codes.rs reads each class's code at the process boundary; a scenario per row would restate the table
* **fuzz:** waived: the input is a closed enum of failure kinds, which the table-driven test walks exhaustively
* **test:** `crates/microvms-cli/src/exit.rs`, `crates/microvms-cli/src/guards/exit_codes.rs`
* **impl:** `crates/microvms-cli/src/exit.rs`
* **live:** `conformance/lanes/local.py`, `conformance/selftest/suite.py`

## CLI-4

Where JSON output is requested, the CLI crate shall emit exactly one envelope object per invocation on stdout, carrying an outcome discriminant and on failure a machine-readable code.

* **model:** waived: one envelope per invocation follows from main's single write, not from a state; crates/model/src/output.rs models the closed-pipe rules, CLI-7 to CLI-9
* **gherkin:** waived: tests/exit\_codes.rs parses stdout as one document at the process boundary, and the live harness does on every call
* **fuzz:** waived: the envelope's count isn't input-driven: one call in main writes it, and the closed-output harness fuzzes what happens around it (CLI-9)
* **test:** `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/tests/exit_codes.rs`, `crates/microvms-cli/tests/thinness.rs`
* **impl:** `crates/microvms-cli/src/commands/attached.rs`, `crates/microvms-cli/src/commands/local.rs`, `crates/microvms-cli/src/commands/mod.rs`, `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/src/main.rs`
* **live:** `conformance/lanes/local.py`, `conformance/selftest/suite.py`

## CLI-5

The CLI crate shall not expose an option that permits a value microvms-core rejects.

* **model:** waived: a property of the parser's closed domains, not of a state
* **gherkin:** waived: the parser tests enumerate each closed domain and round-trip the manifest's published values; a scenario per value would restate them
* **fuzz:** waived: the domains are closed sets the tests enumerate exactly, so there is no open input space to search
* **test:** `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/config.rs`, `crates/microvms-cli/src/manifest.rs`, `crates/microvms-cli/tests/manifest.rs`
* **impl:** `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/commands/local.rs`, `crates/microvms-cli/src/config.rs`, `crates/microvms-cli/src/manifest.rs`
* **live:** waived: a value the parser refuses never leaves the process, so the service never sees it

## CLI-6

If a command is interrupted after a MicroVM has launched, then the CLI crate shall tear down the MicroVM and emit the identifiers of every resource it could not delete.

* **model:** waived: one interrupt in one window of one launch; the guard places it there against a scripted control plane
* **gherkin:** waived: the guard is the scenario: it scripts the control plane, interrupts at RunMicrovm and asserts the exit code, the terminate call, the envelope and the ledger
* **fuzz:** waived: there is no input stream; the window that matters is the one between the launch and RUNNING
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/src/guards/closed_output.rs`, `crates/microvms-cli/src/guards/interrupt.rs`, `crates/microvms-cli/src/ledger.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/commands/agent.rs`, `crates/microvms-cli/src/commands/attached.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`, `crates/microvms-cli/src/exit.rs`, `crates/microvms-cli/src/main.rs`
* **live:** waived: an interrupt has to land between a billable launch and RUNNING, which a live run can't place deterministically; the guard places it at RunMicrovm

## CLI-7

If a reader closes the CLI's stdout or stderr, then the CLI crate shall exit with a status from its exit table and neither panic nor terminate by signal.

* **model:** `crates/model/src/output.rs`
* **gherkin:** `crates/microvms-cli/tests/features/closed_output.feature`
* **fuzz:** `crates/microvms-cli/src/closed_output_fuzz.rs`
* **test:** `crates/microvms-cli/src/closed_output.rs`, `crates/microvms-cli/src/closed_output_fuzz.rs`, `crates/microvms-cli/tests/thinness.rs`
* **impl:** `crates/microvms-app/src/lib.rs`, `crates/microvms-cli/src/closed_output.rs`, `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/src/main.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-domain/src/lib.rs`, `crates/microvms-edges/src/adapters.rs`, `crates/microvms-edges/src/lib.rs`
* **live:** `conformance/lanes/closed_output.py`

## CLI-8

If the reader of stdout or stderr closes after a command has started, then the CLI crate shall perform every teardown and ledger write that command owes and exit with the code of the command's own outcome, except for a streaming command whose stdout reader closes.

* **model:** `crates/model/src/output.rs`
* **gherkin:** `crates/microvms-cli/tests/features/closed_output.feature`
* **fuzz:** `crates/microvms-cli/src/closed_output_fuzz.rs`
* **test:** `crates/microvms-cli/src/closed_output_fuzz.rs`, `crates/microvms-cli/src/guards/closed_output.rs`
* **impl:** `crates/microvms-cli/src/closed_output.rs`, `crates/microvms-cli/src/envelope.rs`, `crates/microvms-cli/src/main.rs`
* **live:** `conformance/lanes/closed_output.py`, `conformance/selftest/closed_output.py`

## CLI-9

If the stdout reader of a streaming command closes, then the CLI crate shall stop streaming within one further event, leave the remote exec running, and exit with ERR\_INTERRUPTED naming the exec id on stderr.

* **model:** `crates/model/src/output.rs`
* **gherkin:** `crates/microvms-cli/tests/features/closed_output.feature`
* **fuzz:** `crates/microvms-cli/src/closed_output_fuzz.rs`
* **test:** `crates/microvms-cli/src/closed_output_fuzz.rs`, `crates/microvms-cli/src/guards/closed_output.rs`
* **impl:** `crates/microvms-cli/src/closed_output.rs`, `crates/microvms-cli/src/commands/attached.rs`, `crates/microvms-cli/src/envelope.rs`
* **live:** `conformance/lanes/closed_output.py`

## COST-1

The cost engine shall carry a provenance label of measured or projected on each duration, with no unlabelled constructor.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: a duration has no unlabelled constructor, and the tests build each label
* **fuzz:** waived: the input is a choice of two labels and a number, which the tests enumerate at the boundaries
* **test:** `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** `conformance/lanes/lifecycle.py`

## COST-2

The cost engine shall not expose an implicit coercion from an estimated dollar amount to a bare float.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: a property of the types' constructors and trait impls, which the compiler holds and a doctest shows failing to compile
* **fuzz:** waived: there is no input stream; the rule is over the type's impls
* **test:** `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** waived: a coercion that doesn't compile can't show up at runtime; the live suite reads dollar figures only as strings

## COST-3

The cost engine shall represent an unpriced quantity as a distinct Unpriced variant carrying the reason, rather than as zero dollars.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the tests build every unpriced line and assert it carries its reason and no figure
* **fuzz:** waived: the unpriced lines are a fixed set the tests enumerate, and the COST-4 property test mixes them with priced ones
* **test:** `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** `conformance/lanes/lifecycle.py`

## COST-4

If an Unpriced amount is summed with an estimated amount, then the cost engine shall produce a lower-bound total that names its unpriced line items rather than a plain sum.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the proptest over every mix of priced and unpriced lines is the specification
* **fuzz:** waived: the proptest `a_total_is_a_lower_bound_exactly_when_something_is_unpriced` searches that space; a coverage-guided harness would search the same one
* **test:** `bindings/microvms-py/tests/test_cost.py`, `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/commands/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** `conformance/lanes/lifecycle.py`

## COST-5

The cost engine shall compute each compute line item from the size class baseline rather than from the peak the guest reports.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the tests price every size class from its baseline and compare with the peak
* **fuzz:** waived: the size classes are a closed table the tests walk row by row
* **test:** `bindings/microvms-py/tests/test_cost.py`, `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-domain/src/cost.rs`
* **impl:** `crates/microvms-domain/src/cost.rs`, `crates/microvms-domain/src/sizing.rs`
* **live:** waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it

## COST-6

The cost engine shall perform money arithmetic in decimal representation, converting each float exactly once at the boundary.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the float boundaries are two functions the tests call directly
* **fuzz:** waived: the proptest `compute_figures_are_exactly_the_decimal_reference` drives the whole arithmetic over generated quantities and checks every figure exactly
* **test:** `crates/microvms-domain/src/cost.rs`
* **impl:** `crates/microvms-domain/src/cost.rs`
* **live:** waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it

## COST-7

While the pinned rate table is older than the staleness window, the cost engine shall attach a staleness warning to each report computed from the stale table.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: staleness is a date comparison the tests make on each side of the window
* **fuzz:** waived: the proptest `staleness_is_the_ninety_day_verdict_and_carries_the_age` covers every age; the window is one threshold
* **test:** `crates/microvms-domain/src/cost.rs`
* **impl:** `crates/microvms-domain/src/cost.rs`
* **live:** waived: the pinned table's age is today minus a committed date, which a live run can't move; the tests pass `today` in

## COST-8

The cost engine shall apply the one-week minimum retention floor to each snapshot storage line item.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the tests price snapshot storage below, at and above the one-week floor
* **fuzz:** waived: the proptest `storage_bills_the_greater_of_the_hold_and_the_retention_floor` covers every hold; the floor is one threshold
* **test:** `crates/microvms-domain/src/cost.rs`
* **impl:** `crates/microvms-domain/src/cost.rs`
* **live:** waived: a pure function of the usage and the pinned rate table; it makes no AWS call, and the unit tests cover it

## COST-9

The cost engine shall price compute from the ARM rate only, rejecting a catalog whose ARM line is missing rather than substituting the x86 rate.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the tests parse catalogs with and without the ARM line and assert the refusal
* **fuzz:** waived: a catalog is a fixed set of named lines, and the tests drop each one the parser needs
* **test:** `bindings/microvms-py/tests/test_cost.py`, `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/constants.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** waived: the rate table is pinned and parsed offline; the Pricing API is never called at runtime

## COST-10

The cost engine shall mark each duration in a plan estimate as projected, so that the resulting report is distinguishable from a measured report.

* **model:** waived: a rule over values and one pure function of a usage and a pinned rate table, not a state
* **gherkin:** waived: no behavior to script: the tests build a plan and assert every duration on its report is projected
* **fuzz:** waived: the proptest `every_duration_in_a_plan_is_projected` generates the plans; a coverage-guided harness would search the same space
* **test:** `bindings/microvms-py/tests/test_cost.py`, `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-cli/src/commands/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-domain/src/cost.rs`
* **live:** `conformance/lanes/local.py`

## IMAGE-1

The microvms-core shall emit the agentd stanza of a wrapped task Dockerfile and of the default Dockerfile from one source.

* **model:** `crates/model/src/wrap.rs`
* **gherkin:** `crates/microvms-core/tests/features/wrap_task_image.feature`
* **fuzz:** `crates/microvms-core/tests/wrap_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`
* **live:** waived: a pure function of Dockerfile text; it makes no AWS call

## IMAGE-2

When a caller wraps a task Dockerfile, the microvms-core shall end the result with the agentd stanza carrying the client's AGENTD\_PORT, preceded by USER root when the task sets another user.

* **model:** `crates/model/src/wrap.rs`
* **gherkin:** `crates/microvms-core/tests/features/wrap_task_image.feature`
* **fuzz:** `crates/microvms-core/tests/wrap_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-cli/src/commands/local.rs`
* **live:** `conformance/lanes/ensure_image.py`, `conformance/lanes/wrapped_user.py`

## IMAGE-3

If a task Dockerfile has no FROM, ends inside an unfinished instruction, or sets a keepalive not under the stream idle timeout, or the wrap options name an invalid port or workdir or ask to inherit a workdir that nothing declares, then the microvms-core shall refuse to wrap the task Dockerfile with an invalid-argument error naming the cause.

* **model:** `crates/model/src/wrap.rs`
* **gherkin:** `crates/microvms-core/tests/features/wrap_task_image.feature`
* **fuzz:** `crates/microvms-core/tests/wrap_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-cli/src/commands/local.rs`
* **live:** waived: a pure function of Dockerfile text; it makes no AWS call

## IMAGE-4

When a caller derives a base image from a Dockerfile, the microvms-core shall take the docker\_ref from the first FROM, keep the managed base image name, and refuse a Dockerfile with no FROM.

* **model:** `crates/model/src/wrap.rs`
* **gherkin:** `crates/microvms-core/tests/features/wrap_task_image.feature`
* **fuzz:** `crates/microvms-core/tests/wrap_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-cli/src/commands/local.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-5

The language bindings layer shall expose wrap\_dockerfile and the from-Dockerfile base image as thin wrappers that raise the refusals of microvms-core as invalid-argument errors.

* **model:** waived: a binding pass-through has no states; core's are modeled as IMAGE-1..4
* **gherkin:** waived: the scenarios are core's (IMAGE-1..4); each binding's tests check the pass-through
* **fuzz:** waived: the binding hands the text unchanged to core's fuzzed function
* **test:** `bindings/microvms-js/__test__/wrap.mjs`, `bindings/microvms-py/tests/test_wrap_dockerfile.py`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`
* **live:** waived: a pure function of Dockerfile text; it makes no AWS call

## IMAGE-6

The microvms-core shall name an ensured image by its prefix and twelve hex characters of a hash over the daemon bytes, the Dockerfile, the build context entries, the base image, and the size class, keeping the artifact content hash of a request without a build context unchanged.

* **model:** waived: a pure function of the build inputs; the name has no states to explore
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** `crates/microvms-core/tests/context_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/ensure.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/ensure.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-7

When a caller supplies a build context directory, the microvms-core shall add each regular file that Dockerfile.dockerignore, or else .dockerignore, does not exclude to an artifact zip with fixed entry dates and modes, skipping each symlink with a warning.

* **model:** waived: reading a directory has no states; the ignore rules are fuzzed against moby's own regex translation instead
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** `crates/microvms-core/tests/context_fuzz.rs`
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/context.rs`, `crates/microvms-edges/src/control/context.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/context.rs`, `crates/microvms-app/src/control/ensure.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-edges/src/control/context.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-8

When the microvms-core ensures an image, the microvms-core shall resolve the image ARN from one caller-identity call per sandbox and upload the artifact to the content-addressed key under the caller's bucket and key prefix.

* **model:** `crates/model/src/image.rs`
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** `crates/microvms-core/tests/context_fuzz.rs`
* **test:** `crates/microvms-app/src/control/ensure.rs`, `crates/microvms-edges/src/control/services.rs`
* **impl:** `crates/microvms-app/src/control/ensure.rs`, `crates/microvms-app/src/control/services.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-edges/src/control/services.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-9

When a describe finds the ensured image ready or building and the caller has not forced a rebuild, the microvms-core shall return the image once it is ready, marked reused, with no upload and no create.

* **model:** `crates/model/src/image.rs`
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the\_plan\_table
* **test:** `crates/microvms-app/src/control/ensure.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/ensure.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-10

If the ensured image has failed or the caller forces a rebuild, then the microvms-core shall delete the image and wait for the name to be free before building, deleting a ready image only under a forced rebuild.

* **model:** `crates/model/src/image.rs`
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the\_plan\_table
* **test:** `crates/microvms-app/src/control/ensure.rs`, `crates/model-conformance/tests/tables.rs`
* **impl:** `crates/microvms-app/src/control/ensure.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-11

If the create of an ensured image is refused because another caller created the name, then the microvms-core shall describe the image again and wait for that build, returning only a ready image, marked reused.

* **model:** `crates/model/src/image.rs`
* **gherkin:** `crates/microvms-core/tests/features/ensure_image.feature`
* **fuzz:** waived: the input space is two callers interleaved against the platform, which crates/model/src/image.rs checks exhaustively; the decision table is ten rows, all pinned by the\_plan\_table
* **test:** `crates/microvms-app/src/control/ensure.rs`
* **impl:** `crates/microvms-app/src/control/ensure.rs`
* **live:** `conformance/lanes/ensure_image.py`

## IMAGE-12

The language bindings layer shall expose ensure\_image as a thin wrapper that returns the image with the reused flag and the context warnings of microvms-core.

* **model:** waived: a binding pass-through has no states; core's are modeled as IMAGE-8..11
* **gherkin:** waived: the scenarios are core's (IMAGE-6..11); each binding's tests check the pass-through
* **fuzz:** waived: the binding hands its arguments unchanged to core's fuzzed functions
* **test:** `bindings/microvms-js/__test__/ensure.mjs`, `bindings/microvms-py/tests/test_ensure_image.py`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`
* **live:** waived: the conformance section drives core's ensure\_image, which each binding forwards unchanged

## STATE-1

When a launch request is accepted, the microvms-core shall transition the lifecycle to PENDING and record the image as existing.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** waived: PENDING between an accepted launch and the hook's report is the client's own record, which a live run sees only as `run` returning; the replay checks it after every call

## STATE-2

When the platform reports that the run hook answered with a success status, the microvms-core shall mark the lifecycle RUNNING and the agent token installed.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`
* **live:** waived: a live run sees the hook's report only as `run` returning with a daemon that answers (AGENTD-2's live check); the client's RUNNING-and-installed record is checked by the replay after every call

## STATE-3

The microvms-core shall install the agent token at most once per VM lifetime.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** waived: the client offers one launch per `Sandbox`; a second install is the daemon's refusal, which AGENTD-3's live check asserts

## STATE-4

While the lifecycle is RUNNING, the microvms-core shall accept a suspend request and transition the lifecycle to SUSPENDING.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`
* **live:** waived: SUSPENDING is the client's record while the platform suspends, and `suspend` returns only once it reads SUSPENDED (STATE-6's live check); the replay checks the transition after every call

## STATE-5

The microvms-core shall not issue a suspend call while the lifecycle is not RUNNING.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/control.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/control.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`
* **live:** waived: a refusal before any call never reaches the service; the model and its replay against `Sandbox` hold it, and the app's tests drive it

## STATE-6

When the platform reports suspension complete, the microvms-core shall mark the lifecycle SUSPENDED.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`
* **live:** `conformance/lanes/suspend.py`

## STATE-7

While the lifecycle is SUSPENDED, the microvms-core shall accept a resume request, reuse the installed agent token, and transition the lifecycle to RUNNING without re-delivering a run-hook payload.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/control.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/control.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** `conformance/lanes/suspend.py`

## STATE-8

When a resume completes, the microvms-core shall invalidate the cached proxy token.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `bindings/microvms-py/tests/test_session.py`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/session.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`
* **live:** waived: the proxy token cache is client state no live response shows; the replay checks it after every call, and the app's tests check the next request mints

## STATE-9

When a terminate request is accepted, the microvms-core shall transition the lifecycle to TERMINATING and record the VM as terminated.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`
* **live:** waived: TERMINATING is the client's record while the platform terminates, and the live terminate checks read TERMINATED (STATE-10's); the replay checks the transition after every call

## STATE-10

When the platform reports termination complete, the microvms-core shall mark the lifecycle TERMINATED.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `crates/microvms-app/src/sandbox.rs`
* **live:** `conformance/lanes/sessions.py`

## STATE-11

The microvms-core shall not return a terminated VM to RUNNING.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/sandbox.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** waived: a refusal before any call never reaches the service; the model and its replay against `Sandbox` hold it, and the app's tests drive it

## STATE-12

If a resume is requested for a suspended MicroVM that the service terminated while it was suspended, then the microvms-core shall issue the resume to the service and report its refusal as a window-closed error naming the state and stateReason that GetMicrovm reports.

* **model:** `crates/model/src/client.rs`
* **gherkin:** waived: the model walks every interleaving of caller requests and platform reports up to two cycles, and model-conformance's replay drives each path against `Sandbox`; a scenario would restate one of those paths
* **fuzz:** waived: the input is a sequence of requests and reports, which the model enumerates exhaustively and the replay drives; there is no byte stream to fuzz
* **test:** `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-cli/src/guards/history.rs`, `crates/model-conformance/tests/client_lifecycle.rs`
* **impl:** `bindings/microvms-js/src/control.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/control.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** `conformance/lanes/state12.py`, `conformance/selftest/state12.py`

## TRAP-1

The microvms-core shall derive each image create token from a value unique per build attempt, with no caller-supplied token override.

* **model:** waived: a fresh value per build attempt, drawn from the entropy port, not a state
* **gherkin:** waived: no scenario can show a token is unique: the tests draw two hundred and find no repeat, and recreating one name sends two distinct tokens
* **fuzz:** waived: the token has no caller input to fuzz: there's no override to feed
* **test:** `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/token.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-core/src/prelude.rs`, `crates/microvms-edges/src/entropy.rs`
* **impl:** `bindings/microvms-js/src/lib.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/control/fake.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/control/token.rs`, `crates/microvms-app/src/control/transport.rs`, `crates/microvms-app/src/entropy.rs`, `crates/microvms-app/src/ledger.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-app/src/testing.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/commands/lifecycle.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-core/src/prelude.rs`, `crates/microvms-domain/src/constants.rs`
* **live:** waived: a replayed token wedges an image in CREATING for about fifteen hours (docs/PLATFORM.md), so a live run can't show the failure it closes; every live build sends a fresh one

## TRAP-2

If an image build remains in CREATING past the stall grace period with every build still PENDING, then the microvms-core shall reject the build wait with an error naming the client-token replay signature.

* **model:** waived: one wait's verdict over a sequence of describe answers, which the tests script
* **gherkin:** waived: the stall is a timed sequence of describe answers, which the tests script against a fake clock; a scenario would restate them
* **fuzz:** waived: the verdict turns on elapsed time and the builds' statuses, which the tests enumerate
* **test:** `crates/microvms-app/src/control/image.rs`
* **impl:** `crates/microvms-app/src/clock.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-domain/src/constants.rs`
* **live:** waived: a stall needs a replayed token's wedged image, about fifteen hours in CREATING (docs/PLATFORM.md)

## TRAP-3

Where guest identity repair is requested, the microvms-core shall set the additional OS capabilities field to the single enum value the pinned service model accepts, via a typed intent flag rather than a free-form capability list.

* **model:** waived: a bool mapped to the one enum value the model accepts, not a state
* **gherkin:** waived: no behavior to script: a typed flag and the request it writes, which the tests assert
* **fuzz:** waived: the input is one bool; there is no input space
* **test:** `crates/microvms-app/src/control/image.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-domain/src/constants.rs`
* **live:** `conformance/lanes/lifecycle.py`

## TRAP-4

The microvms-core shall derive each platform network connector value as a fully-qualified connector ARN for the request region from an enumerated ingress or egress intent, and accept a caller-supplied connector ARN only as a customer-managed egress connector in the request region when the platform egress intent is absent.

* **model:** waived: a derivation from a closed enum and a shape check on caller ARNs, not a state
* **gherkin:** `crates/microvms-core/tests/features/egress_posture.feature`
* **fuzz:** `crates/microvms-app/src/control/posture_fuzz.rs`
* **test:** `crates/microvms-app/src/control/connector.rs`, `crates/microvms-app/src/control/microvm.rs`
* **impl:** `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-cli/src/cli.rs`
* **live:** waived: every live launch sends connectors derived this way, but no named check reads them back; the offline tests assert the recorded requests

## TRAP-5

If a run-hook payload exceeds the ceiling of 4096 bytes that the service model declares, then the microvms-core shall reject the launch locally before any control-plane call, naming the service-model ceiling.

* **model:** waived: a length check against one constant, not a state
* **gherkin:** waived: no behavior to script: the tests cover both sides of the 4096-byte boundary
* **fuzz:** waived: a length against one ceiling, which the boundary tests cover on both sides
* **test:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/microvm.rs`
* **impl:** `crates/microvms-app/src/control/artifact.rs`, `crates/microvms-app/src/control/context.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/sandbox.rs`
* **live:** waived: refused before the first control-plane call, so the service never sees it

## TRAP-6

If the control-plane call in the requested region fails with the null-message AccessDeniedException and the requested region is outside the measured MicroVMs regions, then the microvms-core shall report the error naming the region's service availability and the access policy, the two causes to verify.

* **model:** waived: one branch on a membership test in an error's text, not a state
* **gherkin:** `crates/microvms-core/tests/features/request_and_preflight.feature`
* **fuzz:** waived: the classifier's inputs are a status, an empty message and a region, which the tests enumerate on both sides of the membership test
* **test:** `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/control/transport.rs`
* **impl:** `bindings/microvms-js/src/lib.rs`, `bindings/microvms-js/src/region.rs`, `bindings/microvms-py/src/lib.rs`, `bindings/microvms-py/src/region.rs`, `crates/microvms-app/src/control/image.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/control/transport.rs`, `crates/microvms-app/src/preflight.rs`, `crates/microvms-core/src/lib.rs`, `crates/microvms-core/src/prelude.rs`, `crates/microvms-domain/src/region.rs`
* **live:** waived: the live suite runs in a region AWS was measured running MicroVMs in, so its calls can't produce the response; docs/PLATFORM.md records the response in us-west-1

## TRAP-7

The microvms-core shall read the minted proxy token from the auth-token header map and send the proxy auth header and the proxy port header on each endpoint request.

* **model:** waived: a header read and two headers sent on each request, not a state
* **gherkin:** waived: no behavior to script: the tests assert the headers on the recorded endpoint requests
* **fuzz:** waived: the headers carry a minted token and a port, with no caller input to fuzz
* **test:** `bindings/microvms-py/tests/test_session.py`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/session.rs`, `crates/microvms-app/src/control/fake.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`
* **live:** `conformance/lanes/lifecycle.py`

## TRAP-8

If a MicroVM reaches a terminal state before RUNNING, then the microvms-core shall reject the launch with the state and stateReason attached.

* **model:** waived: the rule is what a refusal carries, the state and its reason, which the tests assert on scripted terminal states
* **gherkin:** waived: the tests drive every terminal state before RUNNING against a scripted control plane; a scenario per state would restate them
* **fuzz:** waived: the input is a closed set of terminal states, which the tests enumerate
* **test:** `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/sandbox.rs`
* **impl:** `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/sandbox.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-domain/src/constants.rs`
* **live:** waived: a VM can't be made to reach a terminal state before RUNNING on demand against the live service

## TRAP-9

The microvms-core shall mint the endpoint proxy token inside the request retry path at an interval strictly below the sixty-minute service ceiling.

* **model:** waived: an interval against a ceiling on the clock port, not a state
* **gherkin:** waived: the refresh is asserted against a fake clock in the tests; a scenario would restate them
* **fuzz:** waived: the interval is a constant against a sixty-minute ceiling, with no input space
* **test:** `bindings/microvms-py/tests/test_session.py`, `crates/microvms-app/src/session/exec.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`, `crates/microvms-core/tests/turmoil_client.rs`
* **impl:** `bindings/microvms-js/src/session.rs`, `bindings/microvms-py/src/session.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-app/src/sandbox.rs`, `crates/microvms-app/src/session/mod.rs`, `crates/microvms-app/src/session/proxy.rs`, `crates/microvms-cli/src/commands/attached.rs`, `crates/microvms-cli/src/seam.rs`, `crates/microvms-edges/src/session/forward.rs`
* **live:** waived: the ceiling is sixty minutes, so a live check would hold a billable session past it to see one re-mint; the tests expire the token on a fake clock instead

## TRAP-10

If a requested minimumMemoryInMiB is not one of the five documented size-class baselines, then the microvms-core shall reject the request locally rather than forwarding an off-table value.

* **model:** waived: a membership check over the five documented baselines, not a state
* **gherkin:** waived: no behavior to script: the tests accept each of the five baselines and refuse the values beside them
* **fuzz:** waived: the baselines are a closed table the tests enumerate, with nothing between rows to search
* **test:** `bindings/microvms-py/tests/test_cost.py`, `bindings/microvms-py/tests/test_smoke.py`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-domain/src/cost.rs`, `crates/microvms-domain/src/sizing.rs`
* **impl:** `bindings/microvms-js/src/cost.rs`, `bindings/microvms-js/src/sandbox.rs`, `bindings/microvms-py/src/cost.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-domain/src/sizing.rs`
* **live:** waived: refused before the first control-plane call, so the service never sees it

## TRAP-11

The microvms-core shall not request a SHELL\_INGRESS connector unless the launch asks for shell access, nor call CreateMicrovmShellAuthToken except to open an interactive shell session.

* **model:** waived: a rule over which operations a lifecycle calls, not over its states
* **gherkin:** waived: no behavior to script: the full-lifecycle test counts every operation and connector a lifecycle sends
* **fuzz:** waived: there is no input stream; the rule is over the calls a lifecycle makes
* **test:** `crates/microvms-app/src/control/connector.rs`, `crates/microvms-app/src/control/microvm.rs`
* **impl:** `crates/microvms-app/src/control/connector.rs`, `crates/microvms-app/src/control/fake.rs`, `crates/microvms-app/src/control/microvm.rs`, `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/transport.rs`, `crates/microvms-edges/src/session/shell.rs`
* **live:** waived: a live run can't see an operation the client didn't call; the recorded lifecycle can, and counts none

## TRAP-12

The microvms-core shall verify each hardcoded service constraint against the pinned botocore service model in the build gate.

* **model:** waived: a comparison of constants with the pinned service model, not a state
* **gherkin:** waived: no behavior to script: the gate compares two JSON documents
* **fuzz:** waived: the inputs are the pinned model and the emitted constants, both fixed
* **test:** `crates/microvms-domain/src/constants.rs`
* **impl:** `crates/microvms-app/src/control/mod.rs`, `crates/microvms-app/src/control/ops.rs`, `crates/microvms-cli/src/cli.rs`, `crates/microvms-cli/src/commands/local.rs`, `crates/microvms-domain/src/constants.rs`, `crates/microvms-domain/src/hooks.rs`
* **live:** waived: the gate reads the pinned model offline and makes no AWS call

## TRAP-13

The sizing model shall read baseline and peak from the documented five-row table rather than computing the peak as four times the baseline.

* **model:** waived: a table lookup, not a state
* **gherkin:** waived: no behavior to script: the tests read each of the five rows
* **fuzz:** waived: the table has five rows, which the tests read exhaustively
* **test:** `crates/microvms-domain/src/sizing.rs`
* **impl:** `crates/microvms-core/src/lib.rs`, `crates/microvms-domain/src/cost.rs`, `crates/microvms-domain/src/sizing.rs`
* **live:** `conformance/lanes/local.py`

## Threats

The threat table in `docs/TRUST.md`, each key marked when this matrix doesn't
trace it.

| Threat | Requirement | Guard | Status |
|---|---|---|---|
| An in-VM process races the platform to the bootstrap hook | AGENTD-1, AGENTD-3 | `crates/agentd/tests/model_conformance.rs::slice_0_of_the_walk_replays_against_the_daemon`, `crates/agentd/src/state.rs::identical_replay_succeeds_and_a_different_token_conflicts` | guarded; a process that starts before the daemon still wins, which is the unenforced invariant below |
| An ordinary exec inherits image privileges its workload does not need | AGENTD-26 | `crates/agentd/src/exec_capabilities.rs::reduction_clears_i_a_and_only_the_seven_bounding_bits` | guarded when the image enables `AGENTD_DROP_EXEC_CAPABILITIES`. It defaults off, and root workloads remain in the daemon's trust boundary |
| A caller holding the agent token but not the host key opens a verified tunnel | AGENTD-17 | `crates/agentd/src/tunnel_identity.rs::only_the_pinned_host_key_completes_a_handshake`, `crates/agentd/tests/tunnel_relay.rs::a_valid_token_with_the_wrong_host_key_is_refused`, `crates/model/src/tunnel.rs::agentd_17_a_token_holder_without_the_host_key_is_refused_before_any_dial` | guarded; under KK no one-sided change turns the pin off, so its seeded fault turns it off in the tunnel model |
| A verified tunnel's handshake fails, or the VM has no key, and the guest service is reached anyway | AGENTD-18 | `crates/agentd/tests/tunnel_relay.rs::a_refused_caller_never_causes_a_guest_connection`, `crates/agentd/tests/tunnel_relay.rs::identity_against_a_seedless_vm_is_refused_not_downgraded`, `crates/model-conformance/tests/tunnel_confirmation.rs::a_handshake_without_confirmation_leaves_the_guest_listener_idle`, `crates/model-conformance/tests/tunnel_end_of_stream.rs::a_verified_tunnel_requires_the_requested_guest_port` | guarded |
| A guest answers a verified tunnel's handshake with a key other than the pinned VM key | BIND-21 | `crates/microvms-core/tests/tunnel_end_to_end.rs::a_wrong_pin_fails_closed_with_a_diagnosis`, `crates/microvms-core/tests/tunnel_end_to_end.rs::a_reply_that_does_not_verify_against_the_pin_fails_the_tunnel` | guarded |
| A guest or the path replays, reorders or forges tunnel frames after the handshake | AGENTD-21, BIND-24 | `crates/agentd/tests/tunnel_relay.rs::agentd_21_a_replayed_frame_ends_the_tunnel_unrelayed`, `crates/agentd/tests/tunnel_relay.rs::agentd_21_a_forged_frame_ends_the_tunnel_unrelayed`, `crates/microvms-edges/tests/tunnel_end_of_stream.rs::bind_24_a_replayed_frame_fails_the_tunnel_unwritten`, `crates/microvms-edges/tests/tunnel_end_of_stream.rs::bind_24_a_forged_frame_fails_the_tunnel_unwritten`, `crates/model/src/tunnel.rs::bind_24_the_model_finds_a_replay_when_frames_carry_no_position`, `crates/agentd/src/tunnel_fuzz.rs::frames_open_in_order_and_the_callers_end_only_after_every_chunk`, `crates/microvms-edges/src/session/tunnel_fuzz.rs::frames_open_in_order_and_the_daemons_end_only_after_every_chunk` | guarded |
| A guest streams hostile server-sent events to the client | BIND-22 | `crates/microvms-app/src/session/sse.rs::an_unterminated_stream_is_refused_at_the_pending_ceiling`, `crates/microvms-app/src/session/sse.rs::an_unrecognized_or_unparseable_frame_is_dropped_rather_than_raised`, `crates/microvms-app/src/session/sse_fuzz.rs::hostile_stream_bytes_stay_bounded_and_every_event_round_trips` | guarded |
| A workload whose caller omits `user` runs as guest root | AGENTD-22, AGENTD-24 | `crates/agentd/src/exec.rs::a_start_that_names_no_user_runs_as_the_default_resolved_per_request`, `crates/agentd/src/exec.rs::a_numeric_default_runs_as_its_row_and_one_with_no_row_is_refused`, `crates/agentd/src/exec_start.rs::a_default_that_names_nobody_is_refused_naming_the_variable`, `crates/model/src/exec_start.rs::an_unknown_default_falling_back_to_the_daemon_starts_as_root`, `crates/model/src/exec_start.rs::a_default_read_as_a_request_string_keeps_the_daemons_group`, `crates/agentd/src/exec_start.rs::captured_numeric_identity_preserves_the_primary_gid_and_explicit_precedence` | guarded when the image sets a non-root `AGENTD_DEFAULT_USER` or preserves a non-root Dockerfile user. An authorized caller can still ask for root |
| A replaced or tampered daemon release asset | BIND-18 | `crates/microvms-edges/src/provision/release.rs::another_signer_identity_is_refused`, `crates/microvms-edges/src/provision/release.rs::one_flipped_byte_in_the_asset_is_refused` | guarded |
| A release directory (`$MICROVM_RELEASE_DIR`) holding an asset and a matching `SHA256SUMS` but no bundle, or another release's files under the requested tag | BIND-18 | `crates/microvms-edges/src/provision/release.rs::a_release_directory_without_its_bundle_is_refused_despite_a_matching_checksum`, `crates/microvms-edges/src/provision/release.rs::another_releases_files_under_the_requested_tag_are_refused` | guarded |
| An on-path party ends a verified tunnel early, with a plaintext close frame or by dropping the connection | BIND-23, AGENTD-19, AGENTD-20 | `crates/microvms-edges/tests/tunnel_end_of_stream.rs::a_verified_tcp_consumer_observes_the_stream_verdict`, `crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_a_close_frame_forged_mid_stream_ends_truncated`, `crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_a_connection_dropped_mid_stream_ends_truncated`, `crates/model-conformance/tests/tunnel_end_of_stream.rs::bind_23_the_daemons_end_of_stream_withheld_ends_truncated`, `crates/model-conformance/tests/tunnel_end_of_stream.rs::agentd_20_the_clients_end_of_stream_withheld_resets_the_guest`, `crates/agentd/tests/tunnel_relay.rs::agentd_19_a_guest_eof_reaches_the_caller_as_the_end_of_stream` | guarded. A protocol 2 peer that omits the end-of-stream offer ends `ClosedUnproven`. Each side refuses a protocol 1 handshake |