diff --git a/docs/design/session-framework/README.md b/docs/design/session-framework/README.md
index ed13a4a..a2a0bd3 100644
--- a/docs/design/session-framework/README.md
+++ b/docs/design/session-framework/README.md
@@ -34,6 +34,15 @@ retroactively to existing [public feed](../../feed-protocol.md),
 6. [Application/presentation boundary](publishing-v1.md) — snapshots, flexible data and effects.
 7. [Implementation guide](implementation.md) — sequenced build tasks and acceptance tests.
 
+Two derived specifications, written by CONTRACT-01 because the slices that need them cannot
+be built without them:
+
+- [Seed derivation v1](seed-derivation-v1.md) — independent per-agent seeds from one recorded
+  master seed and stable agent ids, with test vectors in both languages.
+- [Checkpoint envelope v1](checkpoint-envelope-v1.md) — the exact bytes of the new `FLYSESS1`
+  envelope and the durable commit sequence. `FLYSIM01` is unchanged and stays separately
+  readable.
+
 For context: [modular-session analysis](../malecns-modular-sessions.md) and
 [Melee audit](../melee-framework-audit.md). Each contract owns its named subject; step ordering
 wins over an informal diagram, and Flybus owns transport/resource rules. Resolve contradictions
diff --git a/docs/design/session-framework/checkpoint-envelope-v1.md b/docs/design/session-framework/checkpoint-envelope-v1.md
new file mode 100644
index 0000000..c83bb70
--- /dev/null
+++ b/docs/design/session-framework/checkpoint-envelope-v1.md
@@ -0,0 +1,181 @@
+# Checkpoint envelope v1: `FLYSESS1`
+
+Status: **draft 1**, 2026-09-22. Specified by CONTRACT-01 of the
+[implementation guide](implementation.md); required by
+[session artifacts, native media and recovery](state-media-v1.md) section 4, which says to
+"use a new envelope version; specify exact byte layout before production files". Reference
+implementations of the layout: `services/flysim/crates/fly-session-types/src/checkpoint.rs`
+and `packages/session-types/src/checkpoint.ts`; fixture:
+`.../fly-session-types/fixtures/checkpoint-envelope.json`.
+
+This is the byte layout and the durable commit sequence. The store itself, generations,
+rotation, the writer thread and the capture RPC flow are the STATE-01 slice.
+
+## 1. Why a new format
+
+The historical envelope (`FLYSIM01`, `crates/flybrain-core/src/envelope.rs`) is a magic, a
+`u32` manifest length, a JSON manifest, `u32`-prefixed chunks in manifest order and a CRC32
+footer, with chunk names restricted to ASCII letters so the TypeScript reader can never name a
+prototype key. It stays exactly as it is, and its reader stays separately readable: nothing in
+this document changes a byte of it, and a `FLYSIM01` file is refused by a `FLYSESS1` reader at
+the magic.
+
+A coherent all-participant session checkpoint needs what that format does not have:
+
+- payload names that are `Id`s (`agent-fly-a`, `executor-fly-a`), so the letters-only
+  constraint is widened **deliberately, in a new version**, rather than quietly;
+- a per-payload content digest, because state-media-v1 section 1 makes digests mandatory on
+  checkpoint payloads and a group install must be able to fail one participant's bytes;
+- a payload table with explicit offsets and lengths, so a reader can map one participant's
+  payload without walking every preceding chunk;
+- SHA-256 over the whole prefix instead of CRC32, matching the `Digest` type these contracts
+  already use everywhere else.
+
+## 2. Byte layout
+
+All integers are unsigned little-endian. All digests are raw 32-byte SHA-256 (the manifest
+records the same digests as lowercase hex `Digest` strings).
+
+### Header, 32 bytes
+
+| Offset | Size | Field |
+| ---: | ---: | --- |
+| 0 | 8 | Magic, ASCII `FLYSESS1` |
+| 8 | 4 | `envelopeVersion`, `1` |
+| 12 | 4 | `headerBytes`, `32` |
+| 16 | 4 | `manifestBytes` |
+| 20 | 4 | `payloadCount`, at most 64 |
+| 24 | 4 | `tableOffset` |
+| 28 | 4 | Reserved, must be zero |
+
+### Manifest
+
+`manifestBytes` bytes of canonical JSON (RFC 8785) at offset 32, no trailing newline. It is
+canonical so the envelope's own digest is stable under reserialization, and a reader rejects a
+manifest that is not already canonical rather than silently accepting a second spelling.
+
+### Payload table
+
+At `tableOffset`, which is `32 + manifestBytes` rounded up to a multiple of 8.
+`payloadCount` entries of 112 bytes each, in write order:
+
+| Offset in entry | Size | Field |
+| ---: | ---: | --- |
+| 0 | 64 | Name: an `Id` in ASCII, NUL-padded, no bytes after the terminator |
+| 64 | 8 | `offset` |
+| 72 | 8 | `byteLength` |
+| 80 | 32 | SHA-256 of exactly `byteLength` bytes at `offset` |
+
+### Payloads
+
+Each payload starts at its declared offset. The first starts at the end of the table rounded
+up to a multiple of 8; each subsequent one starts at the previous payload's end rounded up the
+same way. Padding bytes are zero. Offsets are ascending and non-overlapping, which a reader
+checks rather than assumes.
+
+### Footer, 48 bytes
+
+| Offset from end | Size | Field |
+| ---: | ---: | --- |
+| 48 | 8 | `fileBytes`, the total length including the footer |
+| 40 | 32 | SHA-256 of every byte before the footer |
+| 8 | 8 | Magic, ASCII `FLYSESSF` |
+
+A truncated file therefore fails at the footer magic or the recorded length, not at an
+arbitrary payload.
+
+## 3. Manifest fields
+
+State-media-v1 section 4 lists what the manifest records. The names below are the JSON field
+names; a manifest missing any of them is not a complete checkpoint.
+
+| Field | Contents |
+| --- | --- |
+| `envelopeVersion` | `1` |
+| `checkpointId` | `Id`, the identity every participant's capture shares |
+| `sourceScope` | `Scope`: session, epoch and the committed step |
+| `episodeId` | `Id` |
+| `worldTime` | `RationalNs`, the environment's logical time at that boundary |
+| `schedulerId` | The coordinator's scheduler identity, `lockstep-v1` in v1 |
+| `compositionDigest` | Coordinator scheduler and configuration identity |
+| `portMap` | The exact port-to-agent map, `[{portId, agentId}]` |
+| `compatibility` | Backend, content, patch, controller, parser and state-format identities |
+| `agents` | Per agent: profile, dataset and model identities, resolved seed, tick count, remainder and the payload name holding its state |
+| `coordinator` | Task ledger, prior world inspection, per-agent executor state, admission state and event watermarks, each as a payload name or an inline value |
+| `helperState` | External-helper state required for exact resume, as payload names |
+| `payloads` | `[{name, byteLength, digest}]`, mirroring the payload table |
+
+`payloads` is redundant with the table on purpose: the table is what a reader needs to map
+bytes, and the manifest is what a store lists, compares and reports without opening the
+payload area. A reader checks that the two agree.
+
+What the manifest must **not** contain (state-media-v1 section 4): a transient bus `storeId`,
+artifact ID, owner token, mapping or pointer. Payload bytes and durable content identity are
+the only things that survive; on restore the durable store imports fresh bus artifacts, and
+`sourceScope` is provenance, not a claim on the current router.
+
+## 4. What a reader enforces
+
+In this order, so a corrupt file fails on its own terms rather than on a derived value:
+
+1. Length at least header plus footer; magic; version; `headerBytes`; reserved word zero.
+2. Footer magic, `fileBytes` equal to the actual length, and the prefix digest.
+3. Manifest inside the payload area, valid strict JSON (duplicate keys, invalid UTF-8 and
+   non-finite numbers refused) and already canonical.
+4. `tableOffset` exactly at the laid-out position; the table inside the payload area.
+5. Per entry: an `Id` name with no bytes after its terminator, names unique, the declared
+   offset exactly at the aligned end of the previous payload, the payload inside the payload
+   area, and its digest matching its bytes.
+6. No padding between the last payload and the footer.
+7. The required manifest field set, `envelopeVersion` of 1, and a `payloads` list that matches
+   the table name for name, length for length and digest for digest.
+
+Failing any of these is a corrupt or foreign file. The group install rule of state-media-v1
+section 5 then applies: corrupt any participant and installation fails as a group.
+
+## 5. Durable commit
+
+State-media-v1 section 6, in the order the writer performs it:
+
+1. Write the envelope to a temporary generation file in the store directory.
+2. `fsync` the file.
+3. `rename` it to its final generation name.
+4. `fsync` the store directory.
+5. Write the store manifest to its own temporary file, `fsync`, `rename`, `fsync` the
+   directory.
+
+**The store manifest rename is the durable commit point.** Before it, the generation file is
+an unreferenced temporary that is never a restore candidate. After it, and only after it, the
+writer reports a saved acknowledgment and moves the high-water mark.
+
+Consequences the writer must respect rather than reinterpret:
+
+- Bus publications for `captured`, `queued`, `committed`, `failed` and `superseded` are
+  distinct events; only durable completion produces the saved acknowledgment.
+- A lost save reply never advances durable metadata: the coordinator resolves the same
+  operation or fails the epoch, and an unreferenced generation stays unreferenced.
+- A failed write releases its owned ephemeral captures under the configured retry policy and
+  reports the failure. It never reports false durability.
+- The writer owns the bus artifact handles until the bytes are committed or the job fails, and
+  drops them afterwards; durable files are outside the bus's ephemeral collection.
+- No per-payload `fsync` inside one envelope: the single file `fsync` in step 2 covers it.
+
+## 6. Fixture
+
+`fixtures/checkpoint-envelope.json` holds one complete envelope: the manifest, five payloads
+(one agent, one executor, the task ledger, the prior inspection and a world payload), the
+envelope's base64 bytes, its exact layout (header size, manifest offset and length, table
+offset, every entry's offset, length and digest, footer offset, total length) and six
+corruptions a reader must refuse, each naming the byte to flip.
+
+The two implementations are held to it from both directions: each parses the fixture and
+checks every recorded offset, and the TypeScript side re-encodes the same manifest and
+payloads and requires the bytes to be identical to the fixture. A layout change that only one
+language makes therefore fails on the next test run.
+
+## 7. Out of scope
+
+Generations, rotation, hot versus durable copies, the capture queue and its bounds, the
+`State.Capture` / `State.StageRestore` / `State.ActivateRestore` flow, compatibility
+comparison rules and group fencing. Those are STATE-01, over this layout. `FLYSIM01` and the
+legacy composition keep their own format and their own reader, unchanged.
diff --git a/docs/design/session-framework/seed-derivation-v1.md b/docs/design/session-framework/seed-derivation-v1.md
new file mode 100644
index 0000000..97d0680
--- /dev/null
+++ b/docs/design/session-framework/seed-derivation-v1.md
@@ -0,0 +1,101 @@
+# Seed derivation v1
+
+Status: **draft 1**, 2026-09-22. Specified by CONTRACT-01 of the
+[implementation guide](implementation.md), required by
+[worker interfaces](workers-v1.md) section 2 before the real-agent slice. Reference
+implementations: `services/flysim/crates/fly-session-types/src/seed.rs` and
+`packages/session-types/src/seed.ts`; test vectors:
+`services/flysim/crates/fly-session-types/fixtures/seed-vectors.json`.
+
+## 1. What this is for
+
+`Agent.Initialize` takes `seed`, a signed 32-bit integer, matching the current RNG input.
+Workers-v1 section 2 requires that the coordinator derive independent per-agent seeds from
+**its recorded master seed and stable agent IDs** under a versioned algorithm, and that the
+algorithm be specified and tested before the real agent slice. This is that algorithm.
+
+It is a reproducibility rule, not a secret: a run manifest records the master seed in the
+clear, and anyone with the manifest can recompute every agent's seed. It is not a key
+derivation function and must not be used as one.
+
+`seed-derivation-v1` is part of composition identity. Changing any byte of it requires a new
+identifier (`seed-derivation-v2`), because two runs that agree on every other identity but
+disagree here are not the same experiment.
+
+## 2. Inputs
+
+| Input | Type | Source |
+| --- | --- | --- |
+| `masterSeed` | `U64` decimal string | Recorded once per run by the application/supervisor |
+| `agentId` | `Id` | The configured agent identity, stable across restarts and epochs |
+
+Both are the ipc-v1 section 2 scalars. An `agentId` that is not an `Id` is an error, not
+something to normalize. The master seed is the whole 64-bit range: a 32-bit master seed would
+be no wider than the seed it derives.
+
+## 3. Derivation
+
+```text
+material = "flybrain/seed-derivation-v1" LF masterSeed LF agentId LF
+digest   = SHA-256(material)
+lanes    = digest read as eight big-endian uint32 values, in order
+seed     = the first nonzero lane, reinterpreted as a two's-complement int32
+```
+
+`LF` is one `0x0a` byte. `masterSeed` is its canonical decimal form: `"0"`, or no leading
+zero. The prefix is a domain separator, so a digest from this algorithm can never collide with
+one taken over some other pair of strings.
+
+Zero lanes are skipped because the pinned kernel's RNG is an xorshift generator, whose state
+must not be zero: a derivation that could hand out `0` would silently produce a stalled
+generator. If every one of the eight lanes were zero, the material is rehashed with a counter
+suffix (`material || "1" LF`, then `"2" LF`, then `"3" LF`) and the search repeats; no input
+has ever needed it, and four rounds exhausted is an error rather than a fallback seed.
+
+The seed is the *negative* number when the lane's high bit is set. That is deliberate: the
+existing RNG input is a signed 32-bit integer, and half the range is negative.
+
+## 4. Properties
+
+- **Deterministic.** The seed is a function of the two recorded inputs and nothing else: not
+  of wall time, agent order, port assignment, worker process or thread count.
+- **Independent per agent.** Distinct agent IDs give unrelated seeds; there is no arithmetic
+  relationship between `fly-a` and `fly-b` for a caller to exploit or accidentally rely on.
+- **Stable across recovery.** Restore, episode reset and a new epoch do not re-derive a
+  different seed for the same agent ID under the same master seed. The seed is persisted as run
+  configuration and state, and the capture compatibility digest covers the resolved seed
+  (workers-v1 section 2), so a checkpoint cannot be installed into a differently seeded
+  instance.
+- **Equal IDs give equal seeds.** That is the only way to get identical seeds, and workers-v1
+  allows identical seeds only when an experiment declares them. A composition therefore
+  refuses a repeated agent ID rather than quietly sharing a seed between two agents.
+
+Non-properties, stated so nobody assumes them: this is not uniform over the int32 range beyond
+what SHA-256 gives, it is not a stream (one seed per agent per run, not per step), and it says
+nothing about how a model consumes its seed.
+
+## 5. Test vectors
+
+`fixtures/seed-vectors.json` carries the full table: five master seeds (`0`, `1`, `42`, `2^63`
+and the `U64` maximum) across four agent IDs, each with the exact material string, its SHA-256
+and the derived seed, plus one four-agent composition and the inputs that must be refused.
+Both implementations reproduce every row, and each records the material as well as the seed so
+a third implementation can find where it diverges.
+
+The first two rows:
+
+| masterSeed | agentId | material | seed |
+| --- | --- | --- | ---: |
+| `0` | `fly-a` | `flybrain/seed-derivation-v1\n0\nfly-a\n` | 1828176714 |
+| `0` | `fly-b` | `flybrain/seed-derivation-v1\n0\nfly-b\n` | 1218785088 |
+
+Refused: an agent ID that is not an `Id` (uppercase, empty, over 64 characters), a master seed
+that is not a canonical `U64`, and a composition with a repeated agent ID.
+
+## 6. Out of scope
+
+Choosing the master seed, recording it in the run manifest, and the hand-selected explicit
+seeds that workers-v1 allows for the first synthetic composition. This document defines only
+the derivation. A profile that needs several independent streams inside one agent derives them
+from the agent's own seed under its own documented rule; that is a profile concern, not a
+session one.