Business logic

What counts as business logic here, and why the shape is unusual

There are no users, no orders, and no billing accounts in this codebase. The domain rules are trap closures: rules that exist because someone measured AWS Lambda MicroVMs behaving in a way that points away from its own cause, and paid for that measurement once so no caller pays again. A rule here is a refusal that costs a second, standing in for a service answer that costs a build cycle, a poll timeout, or an hour spent auditing a correct IAM policy.

Scope. Everything in this file is application-layer. There is no database, no ORM, and no migration, so there are no DB-side invariants to surface. There is no UI, so there is no form-validation layer. Request validation performed by AWS is out of scope except where this client duplicates it deliberately — which it does in most places, for a measured reason: read 2026-08-07 out of botocore’s validate.py, VALIDATED_METADATA_ATTRS is {'required', 'min', 'document', 'union'}, so max, pattern, and enum violations are serialized, sent, and answered with a ValidationException (microvms-core/src/constants.rs:11-23). And this client never reaches that validator at all: it signs with aws-sigv4 and sends with reqwest, so every model constraint including min is enforced by this crate or by nothing (microvms-core/src/constants.rs:25-31). Deleting a local guard on the assumption that the SDK covers the model reopens the constraint with no visible failure.

The rules are formal requirements first, code second

spec/core.symspec.json carries 51 EARS requirements for microvms-core, every one at status: approved, in six families:

Family	Count	What it governs
TRAP-1 … TRAP-13	13	closures over platform behavior that misleads
STATE-1 … STATE-12	12	the VM lifecycle
COST-1 … COST-10	10	cost honesty
CLI-1 … CLI-6	6	the binary’s surface and its exit contract
ARCH-1 … ARCH-5	5	crate boundaries
BIND-1 … BIND-5	5	what a language binding may not weaken

spec/agentd.symspec.json adds 6 requirements, all status: draft, covering the daemon’s bootstrap and control-token ladder — accept a control request whose token equals the installed one, reject a differing one, reject any control request while none is installed, install on first bootstrap, accept an identical replay, reject a different token.

The spec’s stateModel names five variables: vm_state over PENDING / RUNNING / SUSPENDING / SUSPENDED / TERMINATING / TERMINATED, plus token_installed, image_exists, was_terminated, and bootstrap_count bounded 0..3, all frame: stable. Three lifecycle invariants over that model are proved in Z3 by mise run spec:core, whose recorded run reports 3 constraints proved under hypotheses, 0 violated, 0 unknown (mise.toml:224-226) — that task needs a symspec v5 CLI at an absolute path, so it is deliberately outside mise run check (mise.toml:222-227). The runnable half is stateright, which restates the same three over every interleaving in model/src/client.rs:554-569 and passes under cargo test -p agentd-model. One waiver exists, GTWR_R6_MISSING_UNITS against TRAP-5, because the linter’s unit list does not include bytes.

The strength ladder, and how to read the failure-mode column

Every closure is ranked, strongest first, at microvms-core/src/lib.rs:21-40:

• S1, inexpressible — the mistake cannot be written down: a closed enum, a newtype with no conversion, an absent parameter. An S1 closure cannot regress without a compile error.
• S2, expressible but rejected — the mistake can be written, and the client refuses it locally before any control-plane call, with an error naming the docs/PLATFORM.md finding. Weaker, because the guard is code that can regress, but the cost is seconds rather than a build cycle. Every boundary where a bare integer or string still has to be judged lands here.
• S3, correct by default and overridable — weakest, because it protects only the caller who accepts the default. An S3 closure must state what the override costs. There is exactly one.

Two conventions follow. Every error message names its finding rather than restating the constraint, because the guards exist so a reader can reach the measurement (microvms-core/src/lib.rs:42-48). Every guard has a demonstrated way to fail — a named plausible edit that must turn a specific test red; “delete the feature and the test fails” does not count (microvms-core/src/lib.rs:50-57).

Validations

All row citations are the enforcement site. Where a rule is S1, the “failure mode” column says what a caller cannot write rather than what they are told.

Control-plane request shapes

Nine require_* functions in one module, each guarding a member the pinned service model constrains and the SDK does not check.

Rule	Domain	Citation	Failure mode
maximumDurationInSeconds outside 1..=28800 is refused	Launch	microvms-core/src/control/mod.rs:477-494, constant at microvms-core/src/constants.rs:263	ERR_INVALID_ARG saying a longer session needs a second VM, not a larger number. 28800 is eight hours and the hard ceiling on any one VM’s life
idlePolicy.maxIdleDurationSeconds under 60 is refused	Launch	microvms-core/src/control/mod.rs:748-778, constant at microvms-core/src/constants.rs:241-258	ERR_INVALID_ARG. The model states no maximum and the client adds none; the bound that ends a VM’s life is maximumDurationInSeconds
A Version value that is empty, over 2048 characters, or carries whitespace anywhere is refused	Image build, Launch	microvms-core/src/control/mod.rs:496-542, constants at microvms-core/src/constants.rs:121, :128	Three separate ERR_INVALID_ARG messages. The pattern is [^\s]+, so a version pasted with a trailing newline satisfies “non-empty” and fails; the message names the character it found
A NonBlankString member (codeArtifact.uri, baseImageArn, nameFilter, imageVersion, buildId) that is empty, over 2048 characters, or carries whitespace is refused	Image build	microvms-core/src/control/mod.rs:544-596, constants at microvms-core/src/constants.rs:141, :145	ERR_INVALID_ARG naming the character. A blank nameFilter rides in the query string, where it either 400s or filters differently from what was meant
An identifier that is empty or over 256 characters is refused	Every operation	microvms-core/src/control/mod.rs:598-651, constants at microvms-core/src/constants.rs:174, :183	ERR_INVALID_ARG. An empty identifier is the case that pays for this guard: ten of these members are URI parameters, so an empty one collapses /microvms/<id> onto the listing and a DELETE on a collapsed path is worse
A RoleArn under 20 characters, over 2048, or off-pattern is refused	Image build, Launch	microvms-core/src/control/mod.rs:653-708, constants at microvms-core/src/constants.rs:209, :212, :225	Three messages. The short case says a value that short is almost always a role name; the pattern case names the twelve account digits
A port of 0 is refused; there is no ceiling branch	Image build, Session	microvms-core/src/control/mod.rs:710-746, constants at microvms-core/src/constants.rs:232, :239	ERR_INVALID_ARG. Zero means “let the kernel choose” to a listener and is not a port the platform can forward to. PortNumber.max equals u16::MAX, so a ceiling branch would be unreachable — pinned instead by microvms-core/src/constants.rs:1244
A tag key that is empty, over 128 characters, or off-pattern is refused; a tag value over 256 or off-pattern is refused	Image build	microvms-core/src/control/mod.rs:780-846, constants at microvms-core/src/constants.rs:186, :189, :206	ERR_INVALID_ARG naming the offending key. An empty tag value is legal and an empty key is not, and the two ceilings differ by 2x
An image name that is empty, over 64 characters, or outside [a-zA-Z0-9-_]+ is refused	Image build	microvms-core/src/control/mod.rs:848-878, constants at microvms-core/src/constants.rs:104, :112	Three messages, because the pattern message (“no dots, no slashes”) misleads for a 70-character name containing neither
More than 10 network connectors on a launch is refused	Networking	microvms-core/src/control/microvm.rs:391-399, constant at microvms-core/src/constants.rs:290	ERR_INVALID_ARG. The image-level egress list caps at 1, not 10 (microvms-core/src/constants.rs:292-304), pinned by microvms-core/src/constants.rs:897

ControlPlane::run_microvm runs the identifier, duration, idle-duration, version, and role-ARN guards before it builds a wire body (microvms-core/src/control/microvm.rs:356-374).

Image build and Dockerfile agreement

Five guards compare what this client sends against what the caller’s Dockerfile declares. Every one of them defends against the same failure shape: a build that succeeds, a daemon that logs that it started, and an image that still lands in CREATE_FAILED naming nothing.

Rule	Domain	Citation	Failure mode
inherit_workdir against a base that declares no WorkingDir and a Dockerfile that sets none is refused	Image build	microvms-core/src/control/artifact.rs:234-262	ERR_INVALID_ARG. Measured 2026-08-05: al2023-minimal, python:3.12-slim, and node:20-slim all leave WorkingDir empty, so inheritance inherits / and every relative path resolves somewhere the caller did not mean
A Dockerfile whose FROM is not the selected base image’s docker_ref is refused	Image build	microvms-core/src/control/artifact.rs:524-548	ERR_INVALID_ARG. The build runs the Dockerfile on top of baseImageArn, so a mismatch builds against a base none of the measured platform behavior describes
A Dockerfile whose AGENTD_PORT disagrees with the hooks.port this client sends is refused; an absent variable is checked against the daemon’s own default of 9000	Image build	microvms-core/src/control/artifact.rs:305-348	ERR_INVALID_ARG. Silence is not neutral: the daemon keeps its default for an unset variable, so the absent variable produces the failure for a caller who never typed a port
A Dockerfile AGENTD_SSE_KEEPALIVE_SECS at or above the client’s stream idle timeout is refused	Image build	microvms-core/src/control/artifact.rs:405-445	ERR_INVALID_ARG. Equality is refused too, since an interval equal to the timeout races. The failure it prevents reports the client’s own 60s as though it were the keepalive interval
A Dockerfile with no CMD, or with a non-empty ENTRYPOINT, is refused	Image build	microvms-core/src/control/artifact.rs:483-522	ERR_INVALID_ARG. Weak-form on purpose: it does not check that the CMD names a copied path. The unenforceable half — a base image starting its own process before bootstrap — stays with whoever builds the image
The daemon entry in the build artifact carries mode 0o755 explicitly	Image build	microvms-core/src/control/artifact.rs:1-13, :36-39	Structural. A non-executable binary produces an image whose CMD fails, and the symptom is a run-hook timeout that says nothing about permissions
The agent token has no path into the build artifact	Image build	microvms-core/src/control/artifact.rs:15-23	Unwritable (S1). build_artifact has no parameter that could carry one. The artifact becomes a shared image snapshot, so a per-VM secret in it is a secret shared with every VM; a test scans the produced zip’s raw bytes rather than reviewing the API

Trap closures — control plane

Rule	Domain	Citation	Failure mode
TRAP-1: an image-create or run token is derived from a per-attempt nonce; there is no caller-supplied token parameter	Idempotency	microvms-core/src/control/token.rs:101, :111, :120-148	Unwritable (S1). The parameter does not exist. Minted at microvms-core/src/control/image.rs:187-190 and microvms-core/src/control/microvm.rs:415
TRAP-1: the scope label is truncated at its tail, never its head, and the nonce is never truncated	Idempotency	microvms-core/src/control/token.rs:55-71, :150	Silent truncation of the label only. 64-byte scope plus an 8-byte hex nonce stays under the 128-character clientToken ceiling (microvms-core/src/constants.rs:423)
TRAP-2: an image in CREATING past the stall grace with builds listed, non-empty, and every build still PENDING fails the wait	Image build	microvms-core/src/control/image.rs:318-324, :338-390	ERR_BUILD_WEDGED, naming the clientToken replay signature. A clientToken is a permanent idempotency key, so a replayed create is a no-op: the image sits in CREATING, cannot be deleted, and its only version cannot be dropped. Two images were wedged this way for ~15 hours
TRAP-3: guest identity repair is a bool intent; the client injects the one accepted enum value ["ALL"]	Image build	microvms-core/src/control/image.rs:181-185, microvms-core/src/constants.rs:276-280	Unwritable (S1). There is no capability list a caller can populate, and no way to ask for CAP_SYS_ADMIN alone
TRAP-4: a connector is an enumerated intent that derives a fully-qualified ARN for the request region	Networking	microvms-core/src/control/connector.rs:39-47, :60-83	Unwritable (S1). Two intents (AllIngress, Egress), no free-form string. ConnectorIntent::ALL at :54 is the complete set a test can enumerate
TRAP-5: a runHookPayload over 4096 bytes is refused locally before any control-plane call	Launch	microvms-core/src/control/microvm.rs:161-185, constant at microvms-core/src/constants.rs:83	ERR_INVALID_ARG naming the service-model ceiling. Inclusive, measured 2026-08-07: 4096 passes, 4097 fails. Bytes, not characters. docs/STRATEGY.md, docs/TRUST.md, and the model’s own documentation string all claim 16 KB (microvms-core/src/constants.rs:97), which is wrong by 4x in the dangerous direction — the shape RunMicrovmRequestRunHookPayloadString is the authority
TRAP-6: a region outside the five that carry MicroVMs is refused before the first control-plane call	Region	microvms-core/src/region.rs:38-63, :137-164	S1 for a held Region, S2 at the FromStr boundary. ERR_INVALID_ARG naming the null-message AccessDeniedException finding
TRAP-8: a VM reaching a state in fail_on before the wanted one fails the wait with state and stateReason attached	Launch	microvms-core/src/control/microvm.rs:461-466, :482-500	ERR_LAUNCH_DIED. Fails fast rather than polling to the deadline. Both facts, because either alone is unactionable: the state says the VM is gone, the reason is the only evidence that survives it
TRAP-10: a minimumMemoryInMiB that is not one of the five documented baselines is refused locally	Sizing	microvms-core/src/sizing.rs:25-31, :146-161	S1 for a held SizeClass, S2 at from_baseline_mib. Refused, never snapped to a neighbour: the two plausible service behaviors for 1500 differ in both the memory the guest gets and the rate it is billed at
TRAP-11: CreateMicrovmShellAuthToken is never called and SHELL_INGRESS is never requested	Networking	microvms-core/src/control/connector.rs:16-28, microvms-core/src/control/mod.rs:27-31	Unwritable (S1). No enum variant renders it and no method on ControlPlane calls it. The test counts the calls a full lifecycle makes rather than asserting a refusal
Two hook-timeout families cannot be interchanged: run/resume/suspend/terminate cap at 60s, ready/validate at 3600s	Hooks	microvms-core/src/hooks.rs:56-82, :84-105, constants at microvms-core/src/constants.rs:268, :271	Unwritable across families (S1) — no From, no shared trait. S2 within a family: ERR_INVALID_ARG naming both ceilings, because the caller who hits it nearly always picked a build-hook number
A hook port outside 1..=65535 is refused	Hooks	microvms-core/src/hooks.rs:141-149	ERR_INVALID_ARG naming the model range and version
An architecture other than ARM_64 cannot be requested	Image build	microvms-core/src/control/image.rs:168-172, microvms-core/src/constants.rs:282-287	Unwritable (S1). The enum has one value, so the field is injected rather than accepted — a field could only ever express a request AWS rejects, after the upload
ENABLED on all six hooks is a typed enum value, not a &str literal	Image build	microvms-core/src/control/mod.rs:880-909	Compile error. The literal appeared six times with no constant naming either value, so a typo in one was a ValidationException on a call made after the artifact upload

Trap closures — in-VM session

Rule	Domain	Citation	Failure mode
TRAP-7: the proxy token is read out of the authToken map, never as a string	Session	microvms-core/src/control/microvm.rs:268-283, :300-326, microvms-core/src/session/proxy.rs:14-19	S1: ProxyToken exposes no as_str, no Display, no Deref; the auth value comes out through auth_value(), which names the header it reads (microvms-core/src/session/proxy.rs:177). A missing key is WireKind::AuthTokenMint, which is retryable
TRAP-7: every endpoint request sends both X-aws-proxy-auth and X-aws-proxy-port	Session	microvms-core/src/control/microvm.rs:328-337, microvms-core/src/session/proxy.rs:428-434, :436-461	Structural: headers() returns a two-element array. One without the other is rejected indistinguishably from a bad token, so the header that is wrong is not the header the error mentions
A WebSocket handshake carries the same two facts as three subprotocols, minted through the same cache	Session	microvms-core/src/session/proxy.rs:39-52, :463-496	Structural. The browser WebSocket constructor cannot set a header, so the platform moves both facts into Sec-WebSocket-Protocol and strips all three before forwarding. A second token path would be a second place TRAP-9 has to be got right
TRAP-9: the token is minted inside the request path, through exactly one mint function	Session	microvms-core/src/session/proxy.rs:498-506, :508-560	Structural: headers, headers_for_port, and subprotocols all reach the control plane through token_for. A cache miss is two conditions — stale, or out of scope for the requested port
A refresh interval at or above the 60-minute ceiling is refused at construction	Session	microvms-core/src/session/proxy.rs:356-375, constants at :107, :109-111	S2, ERR_INVALID_ARG. DEFAULT_REFRESH_AFTER is 30 minutes — half the ceiling, not just under it, because refreshing at fifty-nine minutes puts the expiry inside the window between building the headers and the proxy validating them
A mint asks for every port already cached plus the new one	Session	microvms-core/src/session/proxy.rs:532-545	A superset rather than a replacement. Measured 2026-08-15: a token minted for the agent port does not authorize 8080, and reusing it produces 403 Access to port denied — whose WebSocket form is an unreasoned 1006

Cost inputs

Rule	Domain	Citation	Failure mode
COST-1: every duration carries a measured or projected provenance label; there is no unlabelled constructor	Cost	microvms-core/src/cost.rs:419-425	Unwritable (S1). DurationP is an enum whose every variant names its provenance; no From<Duration>, no Default, both pinned by compile_fail doctests at :395-408
COST-2: an estimated dollar amount has no coercion to a bare float	Cost	microvms-core/src/cost.rs:546-578	Unwritable (S1). Private field, no From, no Into<f64>, no Deref. Three compile_fail doctests at :519-545, each pinning its own error code
COST-3: an unpriced quantity is a distinct Unpriced variant carrying a reason, never zero dollars	Cost	microvms-core/src/cost.rs:614-625	S1 by exhaustive match. Zero is a claim about the bill; unpriced is a claim about the documentation
COST-6: gb_decimal is the only place an f64 becomes a Decimal, and it is fallible	Cost	microvms-core/src/cost.rs:138-152	ERR_INVALID_ARG. A negative size would render as a credit; NaN, an infinity, and a magnitude past 28 digits have no decimal reading. EstimatedUsd::new takes a Decimal so it cannot become a third boundary (:553-561)
COST-9: a rate catalog whose ARM compute line is missing is rejected rather than substituted	Cost	microvms-core/src/cost.rs:1191-1199, :1200-1258, :1268-1302	S1 for direct construction — the rate fields are private and there are exactly two doors. S2 at from_catalog, which refuses four ways: a missing ARM line whose x86 sibling is present, a missing line with no sibling, a restated unit, and two products where there was one. The ARM message names the x86 rate it will not substitute and the ~18% error that substituting would introduce
A calendar date arriving from outside the crate is validated against its month’s real length	Cost	microvms-core/src/cost.rs:232-241	S2. 2026-02-30 would otherwise yield a day number for March 2nd and an age two days out

Daemon authorization

Rule	Domain	Citation	Failure mode
A control request whose token equals the installed agent token is accepted	Daemon auth	agentd/src/state.rs:241-249, agentd/src/auth.rs:75-79	Constant-time byte comparison via subtle::ConstantTimeEq (agentd/src/auth.rs:28-33)
A control request whose token differs is rejected	Daemon auth	agentd/src/auth.rs:78	401
A control request while no token is installed is rejected distinguishably from a bad credential	Daemon auth	agentd/src/state.rs:241-249, agentd/src/auth.rs:73, :76	503, never 401 and never 404 — a client maps 404 onto “file not found”, turning a protocol error into a phantom missing artifact
A bootstrap request presenting a token while none is installed installs it	Daemon auth	agentd/src/state.rs:202-212, agentd/src/routes.rs:214-223	200
A bootstrap request presenting a token identical to the installed one is accepted	Daemon auth	agentd/src/state.rs:213-215, agentd/src/routes.rs:224-229	200. The platform may retry its own hook, and answering 409 would fail a launch that is fine
A bootstrap request presenting a different token is refused and changes nothing	Daemon auth	agentd/src/state.rs:216-218, agentd/src/routes.rs:230-233	409, installed token unchanged
A malformed run-hook body, an absent runHookPayload, or a payload that does not parse are each refused	Daemon auth	agentd/src/routes.rs:182-211	400, never 404. The token and the payload carrying it are never logged; the refusal is loggable because RunHookError names a key or a shape and never a value
The Authorization header is parsed and compared on raw bytes, never decoded as UTF-8 first	Daemon auth	agentd/src/auth.rs:40-47	No token extracted, or a mismatch. Never a crash — proved over arbitrary header bytes by agentd/tests/proptest_tar.rs:867, :905, :931, :955
Authorization is decided before the request body is polled, and a rejected body is drained under a cap	Daemon auth	agentd/src/auth.rs:62-89, cap at agentd/src/config.rs:20-24	An unauthenticated caller cannot make the daemon allocate. Draining lets a client’s pooled connection survive an error response; draining without a cap is itself a denial-of-service vector
An unmatched path falls through to the 404 fallback rather than being answered 401	Daemon auth	agentd/src/routes.rs:61-76, :78-79	404. route_layer applies the guard only to matched routes: answering 401 for a typo sends a client chasing credentials
ready, validate, suspend, and terminate hooks answer 200 without regard to bootstrap state	Daemon lifecycle	agentd/src/routes.rs:237-258, :292-295	Always 200. ready and validate are image-build hooks called before any instance exists; gating them on a token fails the build rather than the run

Daemon filesystem and resources

Confinement here is two layers, and the second is the kernel’s.

Rule	Domain	Citation	Failure mode
A tar member path that is rooted, carries a prefix component, or pops past depth zero is refused	File transfer	agentd/src/fs.rs:198-216, refusal at :682	Member rejected, 400. Resolution is lexical component walking, never realpath/canonicalize. A leading / is refused rather than stripped: CPython strips it from a member name, but a caller learns nothing from a rewrite
Every member is created relative to one root descriptor with openat2 and RESOLVE_BENEATH | RESOLVE_NO_SYMLINKS | RESOLVE_NO_MAGICLINKS	File transfer	agentd/src/fs.rs:45-67	ELOOP for a symlink component, EXDEV for a resolution leaving the root; both become a 400 naming the member. This is the layer the lexical one cannot cover: issue #15’s V/a/.. case is judged in-tree by name and lands one level shallower on disk
An absolute symlink or hard-link target is refused outright	File transfer	agentd/src/fs.rs:228-231, :726-729	Member rejected naming “absolute link target”
A relative link target must resolve under the extraction root, from its own base depth	File transfer	agentd/src/fs.rs:218-245	Member rejected. A symlink resolves from its own directory, a hard link from the archive root — different bases, both confirmed against CPython 3.14’s _get_filtered_attrs
An in-tree symlink is created as a symlink with its target preserved verbatim	File transfer	agentd/src/fs.rs:20-43	Accepted. Refusing every link member would break upload_dir for any skills tree or test directory containing one — a worse outcome than the traversal hole it guarded
Device and FIFO members are refused; member count and total uncompressed size are capped	File transfer	agentd/src/fs.rs:41-42, :664, :777, caps at agentd/src/config.rs:37-40	Member or archive rejected, 413. Boundary behavior proved exactly by agentd/tests/proptest_tar.rs:776
The extraction root must be absolute	File transfer	agentd/src/fs.rs:1433-1448	400. A relative root resolves against the daemon’s own working directory, which the caller cannot see
A write that would take the filesystem below the configured reserve is refused before it starts	Disk	agentd/src/disk.rs:66-80, agentd/src/fs.rs:97-106, :804, reserve at agentd/src/config.rs:63-69	507 naming the actual free space. Not 500: a 500 is indistinguishable from a daemon defect, so a client retries it — correct for a defect and actively harmful for a full disk. Zero disables the guard
Every buffer, output capture, stdin write, linger, TTL, and stream window is bounded	Resources	agentd/src/config.rs:11-71	Truncation with a marker, or a bounded refusal. A stdin write that blocks past its timeout gives up rather than pinning a connection for the life of the VM

Confinement is deliberately asymmetric, and the reasoning was argued with a reviewer (agentd/src/fs.rs:4-18). The single-file routes PUT/GET /v1/fs/file are not confined to a root. The same bearer token authorizes POST /v1/exec/start, which runs arbitrary commands as root by design, so a root prefix would add no security while breaking real behavior: harnesses write credentials into home directories, drop config into /etc, and stage scratch in /tmp. The confinement that matters is on PUT /v1/fs/tar, where member paths come out of an uploaded archive rather than from a caller who named them. That gap is where the entire traversal class lives.

CLI parser closures

Rule	Domain	Citation	Failure mode
CLI-5: --memory is a closed value set over the five documented baselines	CLI	microvms-cli/src/cli.rs:231-250, reasoning at :4-19	Unparseable (S1 at the parser). 1500 never reaches a handler. The difference between refusing it at the parser and refusing it in core is a build cycle
CLI-5: --region is a closed value set over the five MicroVM regions	CLI	microvms-cli/src/cli.rs:266-284	Unparseable. --unlisted-region is the named way out, declared conflicts_with = "region" once on a flattened struct so the relationship cannot be forgotten on the twelfth command (:298-331)
The domains are spelled out rather than generated, and a test asserts the enum equals the size table	CLI	microvms-cli/src/cli.rs:13-19, microvms-cli/tests/manifest.rs:90	A domain computed at runtime is invisible to --help, to shell completion, and to the manifest’s choices field. A sixth size class that does not reach cli.rs fails the test rather than shipping unreachable
No --client-token, --capabilities, --connector, or --architecture flag exists	CLI	microvms-cli/src/cli.rs:21-29	Unwritable. Core has no such parameter, so there is nothing to forward. Absence asserted by microvms-cli/tests/thinness.rs:426 and the manifest cross-check
A microvm cp --mode conflicts with --tar; --poll conflicts with every writing flag; --detach conflicts with the shapes that must not return early	CLI	microvms-cli/src/cli.rs:660, :680, :805	Unparseable, pinned by microvms-cli/src/cli.rs:1214, :1266

Invariants

VM lifecycle (the twelve STATE requirements)

Enforced in microvms-core/src/sandbox.rs, whose Lifecycle enum is the spec’s vm_state verbatim and which carries the other four spec variables beside it. Every one of those fields is private and every mutation happens in one of the five lifecycle methods, which is what makes the Z3 and stateright proofs proofs about this struct’s reachable states (microvms-core/src/sandbox.rs:9-17, :96-110, :504-520).

Invariant	Where enforced	Citation
STATE-1: an accepted launch moves the lifecycle to PENDING and records the image as existing	Application, Sandbox::run, after the wire call	microvms-core/src/sandbox.rs:698-706
STATE-2: the platform reporting a successful run hook is what marks the lifecycle RUNNING and the token installed — not the launch call	Application, Sandbox::run, after the wait	microvms-core/src/sandbox.rs:720-724
STATE-3: the agent token is installed at most once per VM lifetime	Application, both sides	microvms-core/src/sandbox.rs:649-661 (a second run on one sandbox is refused); agentd/src/state.rs:202-221 (the daemon’s one-shot bootstrap)
STATE-4: a suspend accepted from RUNNING moves the lifecycle to SUSPENDING before the wait, and after the call	Application, Sandbox::suspend	microvms-core/src/sandbox.rs:769-778
STATE-5: no suspend call is issued while the lifecycle is not RUNNING	Application, before the wire	microvms-core/src/sandbox.rs:758-767
STATE-6: the platform reporting suspension complete marks the lifecycle SUSPENDED; a VM that dies while suspending is recorded as terminated instead	Application, Sandbox::suspend	microvms-core/src/sandbox.rs:790-809, wanted set at microvms-core/src/control/microvm.rs:650
STATE-7: a resume is issued only from SUSPENDED, reuses the installed token, and re-delivers no run-hook payload	Application, Sandbox::resume	microvms-core/src/sandbox.rs:849-854, :859
STATE-8: a completed resume invalidates the cached proxy token, through the endpoint the service just reported	Application, Session::rebind	microvms-core/src/sandbox.rs:875-883, microvms-core/src/session/mod.rs:314-320
STATE-9: an accepted terminate moves the lifecycle to TERMINATING and records the VM as terminated — before the call	Application, Sandbox::terminate	microvms-core/src/sandbox.rs:945-949
STATE-10: the platform reporting termination complete marks the lifecycle TERMINATED	Application, Sandbox::terminate, only when a wait was asked for	microvms-core/src/sandbox.rs:972-976
STATE-11: a terminated VM never returns to RUNNING, checked before the window check and before any call	Application, Sandbox::resume	microvms-core/src/sandbox.rs:840-848
STATE-12: a resume past the launch-time suspended window is refused with the elapsed window named	Application, before ResumeMicrovm	microvms-core/src/sandbox.rs:856-857, :898-926
The suspended-window clock is stamped after the suspend call and before the wait, and cleared on a successful resume	Application, Sandbox	microvms-core/src/sandbox.rs:775-778, :884-887
The three Z3-proved invariants hold over every interleaving: bootstrap at most once, no suspend outside RUNNING, a terminated VM never reaches RUNNING	stateright model	model/src/client.rs:554-569
A locally refused call costs zero wire calls — resume after terminate, resume with the window closed, and the payload count matching the launch count are all checked as counters, not as end states	stateright model	model/src/client.rs:584-598, :623-640
The installed token is never replaced and survives a suspend/resume cycle	stateright model	model/src/client.rs:599-616
image_exists is true exactly when a launch was accepted, and a bootstrapped token implies one	stateright model	model/src/client.rs:570-582

Daemon

Invariant	Where enforced	Citation
The launch environment is installed only on the first bootstrap, under the token lock	Application, AppState::bootstrap	agentd/src/state.rs:196-210. A racer that loses the token cannot win the environment: the winner’s map is in place before any other caller can observe a token installed
The agent token and the launch environment are separate parameters, so no code path can move a byte from one into the other	Application, by signature	agentd/src/state.rs:187-194, agentd/src/routes.rs:166-177
An exec id already present in the registry returns success without spawning a second child, decided under the registry lock	Application, agentd exec	agentd/src/exec.rs:363-377
A poisoned lock is recovered rather than propagated, and the soundness argument is per-lock	Application, agentd state	agentd/src/state.rs:8-66, :76-92
An arbitrary archive never escapes its root and never panics	proptest, 256 cases	agentd/tests/proptest_tar.rs:566
A symlink cannot redirect a member that arrives after it	proptest	agentd/tests/proptest_tar.rs:600
Plain members and in-tree symlinks are always accepted	proptest	agentd/tests/proptest_tar.rs:720
The attacker is never authorized; bootstrap is one-shot; only the installed token is accepted; the control API is closed before bootstrap	stateright model	model/src/lib.rs:443-465
Output is never released before an ack; a retried start never spawns twice; there is one exec entry per id	stateright model	model/src/lib.rs:466-481
Every safety property has a sometimes property beside it, so a green run cannot mean a state space that never reached the interesting states	stateright model	model/src/lib.rs:482-515

Cross-crate and cost

Invariant	Where enforced	Citation
COST-4: an unpriced line routes the whole total to a lower-bound variant that names its unpriced items	Application, one Total::of	microvms-core/src/cost.rs:706-751. Total::AtLeast holds the floor beside the reasons, and Add is implemented only EstimatedUsd + EstimatedUsd, so summing an Amount is a compile error
COST-5: each compute line item is computed from the size-class baseline, never from the peak the guest reports	Application, by reachability	microvms-core/src/cost.rs:1584-1616, accessors at microvms-core/src/sizing.rs:184-205. compute_lines reaches only baseline_gb/baseline_vcpu; reading the peak would overstate the memory line exactly 4x
COST-7: a rate table older than 90 days attaches a staleness warning to every report computed from it	Application, on the report	microvms-core/src/cost.rs:90-95, :961-987, :1510-1512. Carried on the report rather than logged, so a library caller with a log filter and a CLI writing only stderr do not each lose it
COST-8: the one-week minimum retention floor applies to every snapshot storage line item	Application, a field on the rate row	microvms-core/src/cost.rs:104-109, :1627-1657
COST-10: every duration in a plan estimate is marked projected	Application, by type	microvms-core/src/cost.rs:1871-1880, :1908-1913. PlanUsage fields are bare f64 seconds, so there is no field a Measured duration could be written into
ARCH-2: protocol drift between client and daemon fails compilation	Cargo dependency graph	microvms-cli/tests/dependency_direction.rs:179
ARCH-3 / ARCH-4 / BIND-1: cli -> core -> protocol, bindings depend only on core, core depends on neither	Test over cargo_metadata	microvms-cli/tests/dependency_direction.rs:68, :95, :219
ARCH-5: the CLI exports no library target at all	Test over cargo_metadata	microvms-cli/tests/dependency_direction.rs:126
CLI-2: the CLI reaches the control plane and the endpoint proxy only through core, and the guard names which seam door was entered	Injected refusing seam	microvms-cli/src/guards.rs:403, :487; source scan at microvms-cli/tests/thinness.rs:426
The CLI’s direct dependency set contains none of the twelve denylisted transport and signing crates	Test over cargo_metadata	microvms-cli/tests/thinness.rs:96
Only the envelope module and two named exceptions in main write to stdout	Source scan	microvms-cli/tests/thinness.rs:503
CLI-4: one JSON envelope per invocation on stdout, on success, on failure, and on a stream that died before its first event	Spawned-binary test	microvms-cli/tests/exit_codes.rs:154, :198, :233
BIND-5: both bindings preserve provenance-labelled durations, estimate-typed dollars, and the distinct Unpriced value	Application, by absent constructors	microvms-py/src/cost.rs:9, :23-27, :220-241; microvms-js/src/cost.rs:20-31, :52-57. new Duration(3600) is a TypeError, Amount.usd is null for an unpriced line, and to_json/to_dict omit the key entirely rather than emitting a null anything permissive sums as zero
Every constant in constants::as_json is checked against the pinned botocore service model by the build gate (TRAP-12), and the key set is pinned by a test	Build gate plus a key-set test	microvms-core/src/constants.rs:33-46, :589, :693
DEAD_STATES is a strict subset of TERMINAL_STATES, and SUSPENDED is terminal but not dead	Application, pinned by test	microvms-core/src/constants.rs:448, :455, :878
The model-backed and tolerated image-ready state sets are disjoint	Application, pinned by test	microvms-core/src/constants.rs:431, :441, :941
A ledger file is removed only when nothing is outstanding; leaked identifiers are recorded before the delete is attempted	Application, on disk	microvms-cli/src/ledger.rs:1-22
CLI-3: every failure class exits with its own integer and ERR_* string, distinct from ERR_UNEXPECTED	Spawned-binary test plus a classification test	microvms-cli/src/exit.rs:78-101, microvms-cli/tests/exit_codes.rs:29, microvms-cli/src/guards.rs:2949, :3063; published table cross-checked at microvms-cli/tests/manifest.rs:161
Retryability is derived from the error kind rather than stored, so the two cannot drift	Application, one matches!	microvms-core/src/error.rs:111-118, mapping at :358-397

The lifecycle is deliberately runtime-checked rather than typestate (microvms-core/src/sandbox.rs:19-32). A Sandbox<Running> returning a Suspended handle would make STATE-5’s wrong call a compile error, which is strictly stronger on the ladder. But a type whose Rust identity changes on every transition cannot be one #[pyclass], so it would be re-erased into a runtime-checked enum at the binding boundary — and the binding’s copy is the one most callers hit. The part of the typestate idea that costs nothing is kept: the check happens before the wire call, and the test asserts the control-plane call count, which is the observable that distinguishes the two designs.

Calculations

Calculation	Inputs	Output	Citation
Compute cost for a phase, as two separate line items	size class, labelled duration, rate table, phase	vCPU-seconds and GB-seconds line items with estimated dollars	microvms-core/src/cost.rs:1584-1616
Snapshot storage for a hold, with the retention floor applied	phase, GB, labelled hold, rate table	GB-months line item, note naming the floor when it applied	microvms-core/src/cost.rs:1627-1657
Snapshot transfer (write on suspend, read on launch or resume)	phase, line, GB, cycle count, rate table	GB line item, no time component	microvms-core/src/cost.rs:1661-1683
Per-GB-month storage rate, derived from the API’s per-GB-hour quote	catalog entry USD per GB-hour	Decimal USD per GB-month	microvms-core/src/cost.rs:1235-1242, :88
A report’s total	every line item’s phase and amount	Total::Exact, or Total::AtLeast with named unpriced lines	microvms-core/src/cost.rs:726-751
Residency ratio: how many times more a running VM costs than a suspended one	two cost reports	Decimal multiplier	microvms-core/src/cost.rs:1987-1991
Per suspend/resume cycle cost	size class baseline GB, write rate, read rate	EstimatedUsd	microvms-core/src/cost.rs:1993-1999
Break-even suspended hold	size class, rate table	Decimal seconds	microvms-core/src/cost.rs:2013-2027
Rate table age and staleness verdict	retrieval date, today	days, bool, optional warning text	microvms-core/src/cost.rs:961-987
Proleptic-Gregorian day number, for date subtraction without a date crate	year, month, day	i64 days since 1970-01-01	microvms-core/src/cost.rs:279-291
Exact seconds from a Duration, without a lossy float step	std::time::Duration	Decimal seconds	microvms-core/src/cost.rs:120-124
Idempotency token assembly	verb, scope label, 8 random bytes	<verb>-<tail-64-of-label>-<16 hex>	microvms-core/src/control/token.rs:120-148
Connector ARN	intent, region	fully-qualified ARN string	microvms-core/src/control/connector.rs:60-83
Available bytes on a write target’s filesystem	path	u64 bytes	agentd/src/disk.rs:66-80

Compute cost per phase

Both figures read the baseline, never the peak (microvms-core/src/cost.rs:1593-1597). vcpu_quantity = baseline_vcpu × seconds, priced at rates.vcpu_second(). memory_quantity = baseline_gb × seconds, priced at rates.gb_second(). They are two line items rather than one blended GB-second because that is how the pricing page prices them, and a blended figure cannot be reconciled against a Cost Explorer breakdown that keeps them apart (microvms-core/src/cost.rs:940-944). The guest reports the peak and bursts to it, but the peak is charged only for the seconds above baseline actually consumed; this client cannot observe those seconds, so the peak is left out rather than guessed at. The 2 GB class reports 8 GB in the guest (microvms-core/src/sizing.rs:81-86), so reading the peak would overstate the memory line exactly 4x.

A suspended VM gets no compute line at all, rather than a compute line multiplied by zero. A zeroed line would reappear the moment someone changed how a duration is derived (microvms-core/src/cost.rs:1827-1835).

Snapshot storage with the retention floor

billed_seconds = max(held_seconds, floor_seconds) where the floor is one week (microvms-core/src/cost.rs:1635-1637). Then quantity = gb × billed_seconds / SECONDS_PER_MONTH, priced at rates.storage_gb_month(). SECONDS_PER_MONTH is 2628000, which is 730 × 3600 — AWS’s own month. It is spelled out because 30-day and calendar-month conventions both give plausible-looking answers that disagree with the worked examples by a few percent (microvms-core/src/cost.rs:74-80).

When the floor applies, the note quotes the day count off the rate row rather than dividing by 86,400 beside the message. The rate-row field is the only thing that knows how long the window is, so a division written beside the message would keep saying “7-day” after a rate row moved to a fortnight (microvms-core/src/cost.rs:1639-1648, :918-927). Not applying the floor would understate the one line item that dominates a create-and-destroy suite by four orders of magnitude: a 2 GB image deleted after sixty seconds still bills about four cents (microvms-core/src/cost.rs:104-109).

Break-even suspended hold

The least trivial formula in the module (microvms-core/src/cost.rs:2013-2027). running_per_sec = baseline_vcpu × vcpu_rate + baseline_gb × gb_rate. storage_per_sec = baseline_gb × storage_gb_month / SECONDS_PER_MONTH. churn = baseline_gb × (write_rate + read_rate).

The solve is piecewise, because the storage charge behaves differently on each side of the minimum-retention window. Inside the window the storage charge is a constant, so the equation is linear in the hold and the candidate is (churn + floor_sec × storage_per_sec) / running_per_sec. Past the window, storage grows with the hold and the slope changes, so the answer is churn / (running_per_sec − storage_per_sec) instead. Solving only one branch returns a number in the wrong regime.

This is the figure a pool scheduler needs, and a bare “100x cheaper” headline does not show it. Below the break-even hold, suspending and resuming costs more than leaving the VM running, so the conclusion the comparison supports is “avoid churn” rather than “avoid residency” (microvms-core/src/cost.rs:1993-1995).

Why the sizing table is data, not arithmetic (TRAP-13)

Every documented peak is exactly four times its baseline, which makes baseline × 4 look like the obvious simplification. The sizing module must not compute it that way. The regularity belongs to AWS’s current table rather than to the service’s contract, so a sixth row that broke the pattern would get the pattern applied to it, reporting a burst ceiling the service does not offer (microvms-core/src/sizing.rs:13-23).

So SIZE_CLASSES (microvms-core/src/sizing.rs:64-99) is the only place any of the twenty numbers appears, and every accessor reads a row out of it through one lookup. To make the guard falsifiable, row_in and class_for_baseline_in take the table as a parameter (microvms-core/src/sizing.rs:247, :255) so a test can drive the accessors over a table whose peak is not 4x its baseline. A test against the shipped table could not tell a lookup from an arithmetic derivation, because every shipped peak is 4x.

Two float boundaries, and only two (COST-6)

seconds_of (microvms-core/src/cost.rs:120-124) is exact rather than a lossy conversion: a Duration is a whole-seconds count plus a nanosecond remainder, both integers, and the nanosecond division is by a power of ten.

gb_decimal (microvms-core/src/cost.rs:138-152) is the only place an f64 becomes a Decimal. It goes through the float’s decimal string rather than its binary value, because Decimal::try_from(0.1f64) would carry the binary error into every downstream figure. It is fallible rather than lossy: NaN, an infinity, and a magnitude past 28 digits have no decimal reading, and a money figure derived from one of them would be a number nobody could reconcile. EstimatedUsd::new deliberately takes a Decimal and not an f64, so it cannot become a third boundary (microvms-core/src/cost.rs:553-561).

The day-number formula

CalendarDate::day_number (microvms-core/src/cost.rs:279-291) is an era-based proleptic-Gregorian conversion so that date subtraction needs no date crate. The year is shifted to be March-based, which puts February’s variable length last; 719468 is the day number of 1970-01-01 in the era count. Rate-table age is today.days_since(retrieved) over that number (microvms-core/src/cost.rs:962-965).

Policy and gates

• Absent parameters are the primary policy mechanism. The strongest closures are things that do not exist: no client_token parameter (TRAP-1), no capability list (TRAP-3), no SHELL_INGRESS variant and no mint_shell_auth_token method (TRAP-11), no architecture field, no conversion between hook-timeout families, no f64 accessor on a dollar figure (COST-2), no unlabelled duration constructor (COST-1), no Measured field on a plan (COST-10). Where a requirement is about an impl being absent, the check is a program that fails to build — as a compile_fail doctest with a pinned error code, because a bare compile_fail passes for any build failure including a typo in the test. microvms-core/src/cost.rs:395-408, :519-545.

• Local refusal before the wire, always. Every S2 guard fires before the first control-plane call, and where the distinction is observable the test asserts the control-plane call count rather than just the error. microvms-core/src/sandbox.rs:29-32; model/src/client.rs:584-589 states it as a model property.

• One guard list, runnable before the artifact upload. create_image runs after the caller has already uploaded the artifact, so a locally-refusable request refused from inside it has cost the caller the S3 PUT. ControlPlane::preflight is that same list extracted as a pure function of the request, and create_image delegates to it rather than keeping a copy, so the two cannot drift. A caller who skips preflight loses only the upload. microvms-core/src/control/image.rs:144-158, :206-266; asserted with a zero-call count at microvms-cli/src/guards.rs:1468.

• Every refusal names its measurement. A guard’s error message cites the docs/PLATFORM.md section rather than restating the constraint, because the guards exist so a reader can reach the measurement. microvms-core/src/lib.rs:42-48.

• The one S3 escape hatch, and what it costs. Region::unlisted accepts a region this client has not seen carry MicroVMs, because AWS adds regions faster than the list is re-read and a client that refuses a region AWS just launched in is its own kind of wrong. The override costs the diagnostic: if the region does not carry MicroVMs, the first control-plane call answers AccessDeniedException with a null message and the caller spends an hour reading a correct IAM policy. It is a visible enum variant rather than a hidden flag, so a reader of a call site can see someone opted in, and a supported name handed to it comes back as its proper variant so nothing downstream handles two spellings. microvms-core/src/region.rs:38-63, :94-113.

• The region list can be wrong in two directions, and one direction is worse. A missing region refuses a launch AWS would have accepted — the safer direction, still wrong, and what unlisted is for. An extra region is worse, because it re-opens the null-message trap for a name nothing will reject. No API answers the question: get_available_endpoints returns an empty list while get_available_regions returns all 34 Lambda regions, so the list is kept by hand and keeping it right is the whole correctness condition. eu-central-1 does not carry MicroVMs and is one of three regions measured returning the null-message denial (2026-08-07). microvms-core/src/region.rs:20-31.

• A best-effort probe only raises when it has the evidence. TRAP-2’s stall probe fires once, past the grace, and raises only when builds are listed, the list is non-empty, and every build is PENDING. A listing failure returns Ok(()), so the wait continues and the caller gets a plain timeout. Unknown is not empty, and a wedge claim made on a throttled API call sends the reader after the wrong cause. The state field read is buildState, not state, and the deserializer refuses the other spelling. microvms-core/src/control/image.rs:338-390.

• Fail-fast state sets are per-call-site, not global. wait_for_state takes fail_on as a parameter because different callers fail on different states. Suspend wants SUSPENDED and tolerates TERMINATED; resume must pass the dead states only, because failing on SUSPENDED would fail every resume — that is the state the call is made from. This is why constants.rs carries both TERMINAL_STATES and DEAD_STATES. microvms-core/src/control/microvm.rs:440-456, microvms-core/src/sandbox.rs:860-873.

• Token minting lives inside the retry path, and a mint failure is retryable. A proxy token capped at sixty minutes and minted once at construction expires mid-trial, and the rejection is indistinguishable from a dead daemon. Refresh is at half the ceiling rather than just under it, because refreshing at fifty-nine minutes puts the expiry inside the window between building the headers and the proxy validating them. A control-plane throttle at minute thirty must not kill a trial that is otherwise healthy. microvms-core/src/session/proxy.rs:21-37, :107-111, :547-560.

• Credentials never reach a log line, by construction rather than by care. RunHookPayload and both ProxyToken types have hand-written Debug impls that print the byte count or the header names instead of the value. Because RunMicrovmRequest keeps its derive, every struct and error chain that formats one inherits the behavior. The values that do carry a credential — the header pairs and the subprotocol strings — are returned to a caller and stored on nothing, so there is no type whose Debug could leak one; a caller that logs what it was handed is outside what the module can prevent, and both accessors say so. microvms-core/src/control/microvm.rs:70-82, :285-298, microvms-core/src/session/proxy.rs:54-60. The daemon logs the launch-env variable count, never the keys or values (agentd/src/routes.rs:214-221).

• Each authorization failure has its own status code. The daemon answers 503 while no token is installed, 401 for a wrong token, 409 for a bootstrap conflict, and 400 for a malformed hook. It never answers 404, because clients map 404 onto “file not found” and turn a protocol error into a phantom missing artifact. agentd/src/auth.rs:69-79.

• A retried bootstrap of the identical token is success, not a conflict. The platform may retry its own hook, and answering 409 there would fail a launch that is fine. agentd/src/state.rs:94-106, agentd/src/routes.rs:224-229.

• The bootstrap route is unauthenticated on purpose, and its defense is arity. The platform has no credential to present, and its request arrives over loopback indistinguishably from an in-VM process. The defense is that the route can only succeed once. agentd/src/routes.rs:166-171.

• Build hooks are ungated on purpose. ready and validate are image-build hooks called before any instance exists and therefore before any token has been delivered. Gating them on bootstrap state fails the build rather than the run, which is a confusing place to discover the mistake. agentd/src/routes.rs:237-258, microvms-core/src/control/mod.rs:880-886.

• Health is reachable before bootstrap, and busy is the orchestrator’s signal rather than a keepalive. A client needs the contract before it holds a token. And the platform measures idleness by inbound traffic through the endpoint proxy, which terminates outside the guest, so a request an in-VM process sends to this port never reaches the thing counting traffic — an in-guest keepalive route would keep nothing alive and would be discovered as broken by a multi-hour run auto-suspending mid-work. So an orchestrator outside the VM polls, which is real inbound traffic, and reads busy to decide whether to keep polling. The assertion of liveness is repeated and is the caller’s. agentd/src/routes.rs:297-340.

• A resume that finds no installed token is logged loudly rather than treated as routine. Measured 2026-08-05 in us-east-1: the in-memory agent token, the filesystem, exec records, and backgrounded processes all survive a suspend/resume cycle, and the endpoint URL is unchanged. So the normal case is a VM that needs nothing, and the absence of a token would mean the resume behaved like a cold start. The one thing that does change is the guest’s view of time: it observes the whole suspension as a single jump, so any timeout, lease, or TLS session a running command holds expires at once. agentd/src/routes.rs:260-290.

• A poisoned lock is recovered rather than propagated, and the reasoning is per-lock. The daemon is the only channel into the VM — no SSH, no supervisor, no console — so .expect() on a poisoned mutex converts one handler bug into a permanently unreachable VM. The token lock is sound in the strong sense: every write is a whole-value assignment, and recovery cannot install a token, so poisoning is not a bootstrap bypass. launch_env is the same argument and carries nothing that authorizes anything. The execs lock is sound for a narrower reason — the map is not left internally corrupt by a panic in a caller’s closure, but one exec entry may be semantically inconsistent, which limits the blast radius to one exec id. agentd/src/state.rs:8-66, :76-92.

• A panic is caught at the outermost layer, and that is narrow on purpose. Without the catch, a panicking handler drops the connection and the client sees a transport error it cannot distinguish from a dead VM; with it the client gets a 500 and the connection survives. It does not undo the panic, and any std::sync::Mutex the handler held is now poisoned — which is why it pairs with the recovery above. agentd/src/routes.rs:86-95.

• The version header is stamped outside route_layer, so it covers every response. Handler bodies, the 401/503 the auth middleware returns before a handler runs, the 413 the body-limit layer injects, and the 404 fallback. A version header a client only sometimes receives is one it cannot use as a precondition. agentd/src/routes.rs:78-85.

• The extractor-level body limit is disabled and the wire-level layer is the real cap. DefaultBodyLimit does not apply to bodies consumed as a stream, so keeping both would silently truncate JSON control bodies at 2 MiB while leaving tar uploads unbounded. agentd/src/routes.rs:71-76.

• Teardown never raises, and order matters. Sandbox::terminate returns a TeardownReport rather than a Result. It runs where a caller’s finally would, and an error raised there replaces the original failure, which is the one worth reading. The order is VM, then image (retrying, because an image in CREATING refuses deletion), then the log group last, because the service can recreate a group deleted before its image. The log group is named rather than deleted: CloudWatch Logs is not in this crate’s dependency set. microvms-core/src/sandbox.rs:45-53, :932-935, :986-1010.

• There is no Drop that tears down. Rust has no context manager and Drop cannot await. A blocking Drop would deadlock inside a runtime and a spawning one would race process exit. So Drop only warns, naming the id, and the rule is that a caller calls terminate explicitly. microvms-core/src/sandbox.rs:55-60, :1060-1061.

• Leaked identifiers are recorded before the delete is attempted, not after. Recording after loses the identifier when the process dies inside the call, which is exactly the interrupt case the ledger exists for. The file is removed only when nothing is outstanding, because a leftover file is how microvm ls knows there is something to tell the operator about. For a wedged image and a service-created log group the identifier is the remedy; there is no second way to find them. microvms-cli/src/ledger.rs:1-22; CLI-6’s teardown-on-interrupt guarded at microvms-cli/src/guards.rs:824, :917.

• Exec idempotency is opt-in, which deliberately inverts TRAP-1’s shape. The default is a generated exec id, because microvm exec is one shot and an id reused by accident means the second invocation is answered from the first’s record. The stable id is the flag, and what it buys is a retry that is safe across the caller’s own restart. This differs from a control-plane clientToken, whose replay wedges an image permanently and which this CLI does not have at all. microvms-cli/src/cli.rs:634-652, agentd/src/exec.rs:363-377; both halves guarded at microvms-cli/src/guards.rs:2004, :2045.

• Local constants are checked against the pinned service model in the build gate (TRAP-12), and the key names are a contract with a script. constants::as_json publishes every hardcoded constraint keyed with the names scripts/check-model-drift.py reads, and the key set is pinned by a test — because a rename here does not fail compilation, it makes a check silently stop comparing. The two values no model states, MICROVM_REGIONS and SIZE_CLASSES, are compared against pinned literals in the script instead, since a value compared only against itself passes by construction. The gate hard-fails when MODEL_API_VERSION disagrees with the service directory it resolves, rather than skipping: a constraint checked against a different API version is a constraint that was not checked. microvms-core/src/constants.rs:33-46, :52-57, :589, :693.

• A disk write is refused before it starts rather than after ENOSPC. ENOSPC arrives after the filesystem is already full, so by then every other writer in the VM is broken too, including the ones that cannot report anything. It also arrives as a generic io error, so the caller cannot distinguish “the disk is full” from “the daemon is broken” — and retrying is correct for the second case and makes the first worse. agentd/src/disk.rs:4-30.

• A rate table’s staleness warning is a fallback rather than the primary defence. The warning can only say that nobody has looked; a drift check against the Pricing API is what tells you whether a rate moved. Ninety days is the same order as the interval at which AWS has historically restructured Lambda pricing, and the cost of the warning when nothing changed is one line of output. microvms-core/src/cost.rs:50-56, :90-95.

• A rate table is all-or-nothing, and a fetched one is authoritative on rates while still hand-read on rules. A partial table would price a run at less than it costs with no way for the caller to see which field was left stale. The catalog prices line items and says nothing about the one-week storage minimum, a per-request charge, a billing increment, or a free tier, so the retention floor is carried from the constant rather than from the fetch — dropping it there would understate a create-and-destroy suite by four orders of magnitude. microvms-core/src/cost.rs:1191-1199, :1253-1258.

• Four WireKinds collapse onto one exit code deliberately, and Unauthorized is not one of them. A shell cannot act differently on “the daemon rejected the request on its merits” in four flavours, and a caller that can reads data.kind. But a 401’s remedy is a credential rather than a wait, so it maps to ERR_CREDENTIALS: retrying a 401 forever and failing a launch that was 200 ms from ready are the two mistakes the classification exists to prevent. A match on a closed enum has no ordering to get wrong. microvms-core/src/error.rs:358-397, microvms-cli/src/exit.rs:8-9, :41.

See also

• impact analysis — 23 shared source citations
• contract map — 22 shared source citations
• debugging guide — 17 shared source citations
• processes — 14 shared source citations
• public api — 13 shared source citations