diff --git a/changes/unreleased/stress-model-fleet-mode.added.md b/changes/unreleased/stress-model-fleet-mode.added.md
new file mode 100644
index 0000000000..b2a051eb09
--- /dev/null
+++ b/changes/unreleased/stress-model-fleet-mode.added.md
@@ -0,0 +1,13 @@
+- **The satellite-network stress model can be generated as a fleet.** `tools/cmd/stress-model -fleet`
+  declares each orbital plane as occurrences of one of four spacecraft blocks — `part sats :
+  BlockA[400] ordered` — with the as-built values as the block's defaults and stated only on the
+  units that diverge, instead of one `part def` per satellite; the spacecraft, ground segment,
+  requirements and state machine are unchanged, and the ring, inter-plane and downlink connectors
+  are declared once over each collection with `[1]` ends rather than once per satellite pair. `-stats`
+  now reports the spacecraft definitions, the units carrying values of their own and the satisfy
+  assertions in both forms, so the two can be compared: at 12 800 satellites the fleet declares 12 467 elements against
+  2 354 827, and validates in 0.70 s and 184 MB rather than 331 s and 20.3 GB. A guide chapter,
+  `docs/guide/modeling-fleets.md`, shows the constellation both ways and what the
+  runtime does with 12 800 occurrences, and the stress-test record and performance notes carry the
+  measurements. `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in `tests/stressmodel`
+  time the runtime over the fleet form.
diff --git a/docs/guide/README.md b/docs/guide/README.md
index 5bf9dea421..8e3497abc9 100644
--- a/docs/guide/README.md
+++ b/docs/guide/README.md
@@ -14,6 +14,11 @@ Read the chapters in order the first time through; each one builds on the ones b
 10. [Troubleshooting](10-troubleshooting.md) — diagnosing a run that stops early
 11. [Migrating a SysML v1 model](11-migrating-from-sysml-v1.md) — `-convert` from XMI, reading the report, finishing by hand
 
+One topic stands on its own once the chapters are read:
+[Modeling fleets and repeated structure](modeling-fleets.md) — one definition with a
+multiplicity, variants with occurrence counts, per-occurrence values, and what a fleet of
+12 800 occurrences costs to validate and to check.
+
 Chapter 9 does one task in all five clients side by side — Go, Python, Node/TypeScript, Java and
 Rust, in tabs — and then has a section per client for what only that one has.
 [Client libraries](../reference/clients.md) explains which to choose and what each covers.
diff --git a/docs/guide/modeling-fleets.md b/docs/guide/modeling-fleets.md
new file mode 100644
index 0000000000..cbf939aa9b
--- /dev/null
+++ b/docs/guide/modeling-fleets.md
@@ -0,0 +1,317 @@
+# Modeling fleets and repeated structure
+
+A fleet — a constellation of satellites, a production run of vehicles, a rack of
+identical servers — is one design, or a few, built many times with values that
+differ per unit. This chapter shows how to write that in SysML v2 so the model
+declares the design once and the units as *occurrences* of it, what the choice
+costs in declared elements against writing every unit out, and what the
+runtime does with a fleet of 12 800 occurrences today.
+
+## One definition, a multiplicity
+
+The unit of a fleet is a `part def`. The fleet is a usage of it with a
+multiplicity:
+
+```sysml
+part def Spacecraft {
+    attribute catalogId : Integer;
+    part comms : CommsSubsystem;
+    attribute dryMass : Real = eps.mass + adcs.mass + comms.mass;
+}
+
+part def OrbitalPlane {
+    part sats : Spacecraft[400] ordered;
+}
+```
+
+`sats` is one declared element whatever the number in the brackets. Every
+occurrence has the shape `Spacecraft` gives it — the same features, the same
+computed `dryMass`, the same mode machine — and the runtime creates the 400
+objects when the plane is instantiated, not when the model is read.
+
+Occurrences are addressed by position in an ordered collection and as a
+whole for anything that applies to all of them:
+
+```sysml
+sysml> %eval network.plane1.sats#(3).catalogId
+sysml> %eval network.plane0.sats.dryMass      // one value per occurrence
+```
+
+A connector whose ends are collection paths connects the occurrences as a
+whole, and an end multiplicity says how many of them each link joins:
+`connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx` declares
+links that each join one transmitter to one receiver over the fleet's ports,
+and `connect plane0.sats.comms.rf to gs0.uplink` gives every satellite in a
+plane a downlink to one station. What such a connector cannot say is *which*
+occurrence pairs with which: a connector end is a feature chain, not an
+expression, so `sats#(1).comms.crosslinkTx` is not an end, and the pairing a
+per-unit model writes out — unit `i` to unit `i + 1`, unit `i` to the same
+slot of the next plane — has no compact form. When the pairing matters,
+name the occurrences it involves (`part unit0 :> sats`, below) and connect
+those; the runtime realizes a collection connector as one link whose ends
+hold the collections, not as a link per pair.
+
+## Variants as specializations
+
+A fleet is rarely one design. Write each variant as a specialization that
+sets what differs — as *defaults*, so an occurrence that says nothing inherits
+the variant's values and one that diverges can still redefine them:
+
+```sysml
+part def BlockA :> Spacecraft {
+    attribute :>> catalogId default = 40000;
+    part :>> comms {
+        part :>> crosslinkTerminal {
+            attribute :>> mass default = 3.1 [kg];
+            attribute :>> serialNumber default = "CROSSLINKTERMINAL-00000-1";
+        }
+    }
+}
+
+part def BlockB :> Spacecraft { /* … */ }
+```
+
+A plane of block-A spacecraft redefines its fleet to the variant, and the
+occurrence count travels with the plane:
+
+```sysml
+part plane0 : OrbitalPlane {
+    part :>> sats : BlockA { attribute :>> plane = 0; }
+}
+part plane1 : OrbitalPlane {
+    part :>> sats : BlockB { attribute :>> plane = 1; }
+}
+```
+
+A value written with `=` on the variant is fixed for every occurrence and
+cannot be redefined beneath it; write `default =` for anything a unit may
+state for itself, and `=` for what is genuinely a property of the design.
+
+## Per-occurrence values
+
+A unit whose as-built values differ from its variant's — a heavier terminal,
+a serial number — is a member of the fleet that subsets it and redefines the
+values it owns:
+
+```sysml
+part plane0 : OrbitalPlane {
+    part :>> sats : BlockA { attribute :>> plane = 0; }
+    part unit16 :> sats {
+        attribute :>> catalogId = 40016;
+        attribute :>> slot = 16;
+        part :>> comms {
+            part :>> crosslinkTerminal {
+                attribute :>> mass = 19.9 [kg];
+                attribute :>> serialNumber = "CROSSLINKTERMINAL-00016-1";
+            }
+        }
+    }
+}
+```
+
+`unit16` is one of the occurrences of `sats` — the collection still has 400
+members, and the units that subset it are its leading members, so with
+`unit0` and `unit16` declared, `sats#(1)` is `unit0`, `sats#(2)` is `unit16`
+and `sats#(3)` onward read the block's defaults. A diverging unit inherits
+everything it does not state, and it is checked by whatever checks the
+fleet. The cost of the model is now proportional to how many units
+*diverge*, not to how many there are.
+
+What the language also allows, and this implementation does not yet, is to
+carry the per-unit values as one table the fleet binds to — a sequence of
+serial numbers bound to `sats.comms.crosslinkTerminal.serialNumber` so that
+the *n*th occurrence reads the *n*th entry. A binding to a collection path is
+accepted, but a target feature that already carries a default is a binding
+conflict, and a sequence of 12 800 literals written in the source is as long
+as the fleet it describes. Until the runtime can bind a table over defaults,
+write diverging units as above and keep the variant's values as defaults.
+
+## The stress-test constellation, both ways
+
+`tests/stressmodel` (`tools/cmd/stress-model`) generates the
+[satellite-network stress test](../project/satellite-network-stress-test.md)
+in both forms: `-fleet` selects the fleet form. Both state the same
+spacecraft — seven subsystems, twenty components with mass, power draw and
+serial number, the power and data connections between them, a mass and a
+power budget, three requirements with `satisfy` assertions, a mode machine
+every spacecraft exhibits — and the same ground stations. The links differ
+in what they can state: the per-unit form writes every ring link (satellite
+`i` to `i + 1`, closing the ring), every inter-plane link (slot `i` to slot
+`i` of the next plane) and every downlink (satellite `i` to station `i mod
+G`) as its own connector, and the fleet form declares one connector per
+collection with `[1]` ends — each link joins one satellite to one satellite
+or station, but the connector does not say which pairs, and the runtime
+realizes it as one link over the collections.
+
+**One definition per satellite.** Every satellite is its own `part def`
+specializing `Spacecraft` and redefines the whole tree beneath it to state
+its serial numbers and as-built masses; the network is a usage of each:
+
+```sysml
+part def Sat0 :> Spacecraft {
+    attribute :>> catalogId = 40000;
+    part :>> eps {
+        part :>> solarArray {
+            attribute :>> mass = 2.0 [kg];
+            attribute :>> serialNumber = "SOLARARRAY-00000-0";
+            // …
+        }
+        // …
+    }
+    // … about 180 declared elements per satellite, its links and requirements included
+}
+part def Sat1 :> Spacecraft { /* … */ }
+part def Network {
+    part sat0 : Sat0;
+    part sat1 : Sat1;
+    interface ring0To1 : RFLink connect sat0.comms.crosslinkTx to sat1.comms.crosslinkRx;
+    // …
+}
+```
+
+**Fleet.** Four spacecraft blocks carry the as-built values as defaults; each
+orbital plane is `part sats : Block[N] ordered` with one ring connector over
+the collection, one connector between adjacent planes and one downlink
+connector per plane and station, their ends declared `[1]` so that each link
+joins one satellite to one satellite or station; every sixteenth unit states
+a catalog number, a slot and a crosslink terminal of its own — the fifteen
+units between read the block's values, so the fleet carries fewer distinct
+per-unit values than the per-satellite form, the trade-off a bound value
+table would remove; the requirements are declared once per block and
+asserted on the block's configuration and on every diverging unit:
+
+```sysml
+part def OrbitalPlane {
+    attribute plane : Integer;
+    part sats : Spacecraft[400] ordered;
+    interface ring : RFLink connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx;
+}
+part def Network {
+    part plane0 : OrbitalPlane {
+        part :>> sats : BlockA { attribute :>> plane = 0; }
+        part unit0 :> sats { /* as-built values */ }
+        part unit16 :> sats { /* … */ }
+    }
+    // …
+    interface plane0To1 : RFLink connect [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx;
+    interface downlink0To0 : RFLink connect [1] plane0.sats.comms.rf to [1] gs0.uplink;
+}
+satisfy blockAMass by blockAConfig;
+satisfy blockAMass by network.plane0.unit16;
+```
+
+`-stats` reports the element count of either form — the number of
+declarations the source makes:
+
+```bash
+go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -stats > legacy.sysml
+# satellites=1600 definitions=1600 units=1600 ground-stations=20 components=32080 connections=25400 requirements=4800 assertions=4800 elements=294627 bytes=18135413
+go run -C tools ./cmd/stress-model -planes 8 -satellites 200 -ground-stations 20 -fleet -stats > fleet.sysml
+# satellites=1600 definitions=4 units=104 ground-stations=20 components=264 connections=220 requirements=12 assertions=324 elements=3203 bytes=192698
+```
+
+| satellites | planes × per plane | form | definitions | units stating values | elements | source |
+| ---------- | ------------------ | ---- | ----------- | -------------------- | -------- | ------ |
+| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB |
+| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB |
+| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB |
+| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB |
+
+The fleet form of the 12 800-satellite constellation is **12 467 declared
+elements against 2 354 827** — a factor of 190 — and what remains grows with
+the number of planes (links, downlinks) and of diverging units, not with the
+number of satellites. (The
+[stress-test record](../project/satellite-network-stress-test.md)'s
+single-definition counts, 299 137 and 2 392 417, are the same constellation
+split differently into planes and stations; the counts here are the same
+layout in both forms.)
+
+## What it costs to validate
+
+All figures below were taken on one machine — `Intel Xeon Platinum 8559C`,
+8 CPUs, 31 GiB of memory, no swap, Go 1.25, Linux — from the binary
+`make build` produces, as single runs; peak RSS is measured from outside with
+`/usr/bin/time`.
+
+`sysml -validate -memstats`, both forms over the layouts above:
+
+| satellites | form | elements | wall | allocated | peak RSS |
+| ---------- | ---- | -------- | ---- | --------- | -------- |
+| 1 600 | one definition per satellite | 294 627 | 22.7 s | 6.2 GiB | 2.5 GB |
+| 1 600 | fleet, 8 × 200 | 3 203 | 0.22 s | 102 MiB | 108 MB |
+| 12 800 | one definition per satellite | 2 354 827 | 331 s | 49.8 GiB | 20.3 GB |
+| 12 800 | fleet, 32 × 400 | 12 467 | 0.70 s | 289 MiB | 184 MB |
+
+Validation is a function of what the source declares, so the fleet form
+validates the 12 800-satellite constellation in **0.70 s and 184 MB** where
+the single-definition form takes 331 s and 20.3 GB. That is the whole
+payoff of writing the model this way, and it is available today.
+
+## What the runtime does with 12 800 occurrences today
+
+Declaring the fleet does not make the satellites free; it moves their cost
+from the source to the runtime, which pays it when something asks for the
+occurrences. Today the runtime materializes an object per occurrence with a
+value slot per feature — the same objects the single-definition form would
+create — and shares only the *shape* of the type (its effective feature list)
+between them. Measured on the same machine, same layouts as above:
+
+| satellites | operation | wall | allocated | peak RSS |
+| ---------- | --------- | ---- | --------- | -------- |
+| 1 600 | `-instantiate` the network | 0.44 s | 238 MiB | 195 MB |
+| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666 MiB | 306 MB |
+| 1 600 | `%eval` of `sats.dryMass` in every plane | 1.85 s | 2.9 GiB | 737 MB |
+| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB |
+| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB |
+| 12 800 | `%eval` of `sats.dryMass` in every plane | 42.7 s | 141.3 GiB | 5.2 GB |
+
+What the rows say about the current runtime:
+
+- **Instantiating** the network (`sysml -instantiate
+  SatelliteNetwork::Constellation::network`) creates the object per
+  occurrence in every plane, 2.06 s and 801 MB — about 60 KB per
+  occurrence, linear from 1 600 to 12 800. The run then warns that
+  materialization is bounded: the walk that reads the created object's
+  feature values stops at the runtime's materialization budget, so the
+  component trees beneath the occurrences are unread, not checked clean.
+- **Checking** an assertion on a unit — `satisfy blockAMass by
+  network.plane0.unit16` — reads the unit through the network object and
+  evaluates its summed mass and power, which materializes the unit's
+  subsystems and components and starts their behaviors. Every check then
+  drains the behaviors the network's objects run, so a check costs more the
+  more of the fleet earlier checks have touched: 2 MiB allocated per
+  assertion in a network of 8 planes, 10 MiB in one of 32 planes. The 2 412
+  assertions of the 12 800-satellite fleet cost 8.84 s and 23.4 GiB
+  allocated, against 83 s and 28.9 GiB for the 9 600 assertions of a
+  3 200-satellite single-definition constellation; each assertion still
+  pays for the fleet around it.
+- **Reading a value over every occurrence** — the dry mass of all 12 800
+  satellites — evaluates the summed expression over the full component tree
+  of every occurrence, 42.7 s and 141.3 GiB allocated. This is the cost the
+  single-definition form paid at validation; the fleet form pays it at the
+  first read instead.
+- A connector over the collection is realized as **one link whose ends hold
+  the collections** (`%eval network.plane0.ring.a` is the sequence of every
+  transmitter in the plane), whatever its end multiplicities declare. The
+  per-pair topology of the single-definition form — `ring0To1`, `ring1To2`,
+  …, `downlink5To0` — is not recovered from it; only what the connector
+  states about the collections as a whole is.
+- A `satisfy` whose subject is the fleet itself (`satisfy blockAMass by
+  plane0.sats`) is rejected: the subject must denote one object. Assertions
+  are therefore made on the block's configuration — one check for every
+  occurrence that inherits the block's values — and on each diverging unit.
+- A collection whose lower bound exceeds 1 000 is not materialized: a plane
+  written `Spacecraft[1600]` validates but its assertions report
+  `multiplicity violation: lower bound too large or infinite` when checked.
+  Keep a fleet under that bound per usage — 32 planes of 400 rather than 8
+  of 1 600 — until the runtime holds occurrences sparsely.
+
+What would make these cheap is described in
+[scaling to very large models](../project/large-model-scaling-design.md),
+one definition, many occurrences: an occurrence whose feature holds its
+block's default storing nothing for it, and a check over N occurrences that
+read only block-level values evaluating once. Until that lands, model the
+fleet as this chapter shows — the declared model is nearly two hundred times
+smaller and validates in under a second — and expect instantiation and
+checking to cost what they cost for the same number of fully written
+satellites.
diff --git a/docs/internals/performance.md b/docs/internals/performance.md
index 09dd7bdb59..bd59b9381d 100644
--- a/docs/internals/performance.md
+++ b/docs/internals/performance.md
@@ -176,6 +176,28 @@ which report nothing:
 Both time and memory grow linearly with the model. Loading was quadratic once —
 doubling the model roughly quadrupled the time — for the reasons below.
 
+Because the cost is per declared element, the largest lever a model has is to
+declare less: one definition with a multiplicity rather than a definition per
+unit. The satellite-network generator writes its constellation both ways
+(`tools/cmd/stress-model -fleet`), and on the machine named above — 8 CPUs, 31 GiB,
+no swap — `sysml -validate -memstats` of the 12 800-satellite constellation
+costs:
+
+| form | elements | source | wall | allocated | peak RSS |
+| ---- | -------- | ------ | ---- | --------- | -------- |
+| one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 331 s | 49.8 GiB | 20.3 GB |
+| four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 771 KB | 0.70 s | 289 MiB | 184 MB |
+
+The runtime then pays for the occurrences when something asks for them: the
+same network instantiates in 2.06 s and 801 MB, its 2 412 `satisfy`
+assertions check in 8.84 s and 23.4 GiB allocated, and reading one summed
+attribute over every occurrence costs 42.7 s and 141.3 GiB, because each
+occurrence is still an object with a value slot per feature whose component
+tree is materialized to evaluate it. Both forms, their element counts and
+what the runtime does with 12 800 occurrences are in the
+[stress-test record](../project/satellite-network-stress-test.md) and the
+guide chapter on [modeling fleets](../guide/modeling-fleets.md).
+
 ### What made it quadratic
 
 The load path had several costs, including three scans over a namespace's
diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md
index 3ee284c264..32dfc7b3f0 100644
--- a/docs/project/satellite-network-stress-test.md
+++ b/docs/project/satellite-network-stress-test.md
@@ -19,7 +19,7 @@ smallest models carry ±30% of noise from the machine, which the trend does not.
 
 ```bash
 go run -C tools ./cmd/stress-model -planes 8 -satellites 25 -ground-stations 20 -stats > constellation.sysml
-# satellites=200 ground-stations=20 components=4080 connections=3175 requirements=600 elements=37552 bytes=2297852
+# satellites=200 definitions=200 units=200 ground-stations=20 components=4080 connections=3175 requirements=600 assertions=600 elements=37552 bytes=2297852
 sysml -validate -memstats constellation.sysml
 sysml -satisfy -memstats constellation.sysml
 ```
@@ -226,6 +226,126 @@ per-document work was about 10 s of 128 s on one job. The per-document gather
 cache (`passes.Gathers`) removed the quadratic term for the editor path, and
 handing one such gather to a batch's workers removed it for the command line.
 
+## The same constellation as a fleet
+
+Everything above declares a `part def` per satellite. The generator's
+`-fleet` form states the same constellation the way a fleet is engineered
+— a few spacecraft blocks carrying the as-built values as defaults, each
+orbital plane as `part sats : Block[N] ordered`, as-built values only on the
+units that diverge from their block (every sixteenth), the ring link as one
+connector over the collection, one inter-plane link per adjacent pair of
+planes and one downlink per plane and station — the collection connectors
+with `[1]` ends, so each link joins one satellite to one satellite or
+station, though not which to which — and the three requirements
+declared once per block and asserted on the block's configuration and on
+every diverging unit. `-stats` reports both forms alike; the new fields are
+the spacecraft definitions, the units that state values of their own, and the
+satisfy assertions, which in the fleet form outnumber the requirements by
+three per unit.
+The guide chapter [modeling fleets](../guide/modeling-fleets.md) shows the
+source of both forms.
+
+```bash
+go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -stats > legacy.sysml
+# satellites=12800 definitions=12800 units=12800 ground-stations=20 components=256080 connections=204400 requirements=38400 assertions=38400 elements=2354827 bytes=145364954
+go run -C tools ./cmd/stress-model -planes 32 -satellites 400 -ground-stations 20 -fleet -stats > fleet.sysml
+# satellites=12800 definitions=4 units=800 ground-stations=20 components=960 connections=724 requirements=12 assertions=2412 elements=12467 bytes=770621
+```
+
+| satellites | planes × per plane | form | definitions | units | elements | source | `-validate` wall | allocated | peak RSS |
+| ---------- | ------------------ | ---- | ----------- | ----- | -------- | ------ | ---------------- | --------- | -------- |
+| 1 600 | 8 × 200 | one definition per satellite | 1 600 | 1 600 | 294 627 | 18.1 MB | 22.7 s | 6.2 GiB | 2.5 GB |
+| 1 600 | 8 × 200 | fleet | 4 | 104 | 3 203 | 193 KB | 0.22 s | 102 MiB | 108 MB |
+| 12 800 | 32 × 400 | one definition per satellite | 12 800 | 12 800 | 2 354 827 | 145 MB | 331 s | 49.8 GiB | 20.3 GB |
+| 12 800 | 32 × 400 | fleet | 4 | 800 | 12 467 | 771 KB | 0.70 s | 289 MiB | 184 MB |
+
+The single-definition rows here are the plane and station layout the fleet
+uses, so the two forms describe the same planes and stations; the validation table above
+(299 137 and 2 392 417 elements, 19.0 s and 318 s) was taken over a layout
+with a different split into planes and stations, and so slightly more links
+and station components. The fleet form
+declares **190 times fewer elements** at 12 800 satellites and validates in
+0.70 s and 184 MB rather than 331 s and 20.3 GB: validation is a function of
+what the source declares, and the fleet source is the size of four
+spacecraft, twenty stations and the links between thirty-two planes.
+
+What the current runtime does with the 12 800 occurrences, on the same
+machine:
+
+| satellites | operation | wall | allocated | peak RSS |
+| ---------- | --------- | ---- | --------- | -------- |
+| 1 600 | `-instantiate` the network | 0.44 s | 238 MiB | 195 MB |
+| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666 MiB | 306 MB |
+| 1 600 | `%eval` of `plane<i>.sats.dryMass`, all 8 planes | 1.85 s | 2.9 GiB | 737 MB |
+| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB |
+| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB |
+| 12 800 | `%eval` of `plane<i>.sats.dryMass`, all 32 planes | 42.7 s | 141.3 GiB | 5.2 GB |
+
+The runtime shares one shape — the effective feature list `FeaturesOf`
+caches per type — between the occurrences of a block, and nothing else: each
+occurrence is an object with a value slot per feature, materialized lazily.
+Instantiating the network is therefore linear and cheap (about 60 KB per
+occurrence; the walk of the created object's feature values stops at the
+materialization budget and says so). Checking is not: a `satisfy` on a unit
+reads the unit through the network object, evaluates its summed mass and
+power — materializing its subsystems and components and starting their
+behaviors — and then drains the behaviors every object of the network runs,
+so each check costs more the more of the fleet earlier checks have touched
+(2 MiB allocated per assertion in a network of 8 planes, 10 MiB in one of
+32 planes): the cost is in evaluating the requirements' expressions, in
+starting the behaviors of the parts that evaluation materializes, and in
+polling the running mode machines. Reading one summed attribute over every
+occurrence evaluates it over the full tree of each — the cost the
+single-definition form paid at validation, paid here at the first read.
+
+Three limits of the current language and runtime shape the fleet form:
+
+- A connector end is a feature chain, so the fleet form cannot write the
+  single-definition form's pairing — `ring<i>To<i+1>` closing each plane,
+  `plane<i>To<j>` between the same slots of adjacent planes, `downlink<i>To<k>`
+  to station `i mod G` — without naming every occurrence. It declares one
+  connector over each collection instead, and the runtime realizes that as
+  one link whose ends hold the collections (`%eval network.plane0.ring.a`
+  is every transmitter of the plane), whatever the `[1]` ends declare. The
+  topology the two forms state is therefore not the same: the fleet says
+  each satellite is linked within its plane, to the next plane and to the
+  stations, not to which neighbour or station.
+
+- A `satisfy` whose subject is a collection (`satisfy blockAMass by
+  plane0.sats`) is rejected — the subject must denote one object — so the
+  fleet asserts each requirement on the block's configuration, which stands
+  for every occurrence inheriting the block's values, and on each diverging
+  unit.
+- A collection whose lower bound exceeds 1 000 (`maxMaterializedLowerBound`)
+  is not materialized: a plane of `Spacecraft[1600]` validates, but checking
+  a unit of it reports `multiplicity violation: lower bound too large or
+  infinite`. The 12 800-satellite fleet is therefore 32 planes of 400.
+
+`BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in
+`tests/stressmodel` measure, warm, instantiating the fleet network and
+reading `sats.dryMass` over four planes, and re-checking every assertion:
+
+```bash
+go test ./tests/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x
+```
+
+| satellites | elements | instantiate + read four planes | per satellite | allocated | assertions | warm re-check | allocated |
+| ---------- | -------- | ------------------------------ | ------------- | --------- | ---------- | ------------- | --------- |
+| 32 | 1 179 | 29 ms | 0.9 ms | 18.4 MiB | 24 | 0.9 ms | 0.5 MiB |
+| 128 | 1 715 | 87 ms | 0.7 ms | 93.1 MiB | 36 | 1.2 ms | 1.0 MiB |
+| 512 | 3 947 | 460 ms | 0.9 ms | 882 MiB | 108 | 8.5 ms | 7.3 MiB |
+
+Warm, instantiating a fleet and reading a summed attribute over its
+occurrences costs **about 1 ms and 1.7 MiB per satellite** — of the order
+of the per-satellite cost of a cold `-satisfy` over the single-definition
+form — because every
+occurrence's component tree is still materialized to evaluate the sum. What
+would change that is sparse per-occurrence values and verification over
+distinct shapes ([scaling to very large models](large-model-scaling-design.md),
+one definition, many occurrences): an occurrence whose feature holds its
+block's default storing nothing for it, and a check over N occurrences that
+read only block-level values evaluating once.
+
 ## Editing: what an editor pays per keystroke
 
 An editor does not validate once; it re-validates the open file after every
@@ -264,7 +384,9 @@ frame in the resolver, its memoized semantics and its gathered facts stay.
 
 The worst edit is to a document everything else depends on. `Split` writes the
 same network as one document per plane beside the library they build on and
-the constellation joining them (six files at these sizes); `BenchmarkLoadFiles`
+the constellation joining them (six files at these sizes; the fleet form, whose
+planes are members of the network, splits into the library and the
+constellation alone); `BenchmarkLoadFiles`
 opens and analyzes every file through one workspace, and `BenchmarkEditImported`
 edits the library and then asks every file for its diagnostics, as the editor's
 refresh sweep does:
@@ -373,9 +495,12 @@ the interactive band at every operation measured.
 - Most figures are for the whole constellation as one file. The split by
   plane is measured above at two sizes only; an editor also pays the per-file
   analysis once per open file.
-- `-satisfy` instantiates each satellite's tree on its own; it does not
-  instantiate the whole `Network` as one object with 12 800 satellites and
-  their links, and no figure here says what that would cost.
+- `-satisfy` over the single-definition form instantiates each satellite's
+  tree on its own; it does not instantiate the whole `Network` as one object
+  with 12 800 satellites and their links. Only the fleet section
+  instantiates the network whole, and its occurrences are lazily materialized
+  objects whose component trees are read only where a check or an
+  evaluation reaches them.
 - Runtime execution is a mode machine driven to its initial state per
   instantiation, not a long simulation with events. Event throughput is
   measured separately in `docs/project/execution-performance-2026-09.md`.
diff --git a/mkdocs.yml b/mkdocs.yml
index dab761c75c..374cc1ed11 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -172,6 +172,7 @@ nav:
       - guide/09-clients.md
       - guide/10-troubleshooting.md
       - guide/11-migrating-from-sysml-v1.md
+      - guide/modeling-fleets.md
   - Document generation:
       - manual/README.md
       - Introduction and concepts: manual/introduction.md
diff --git a/tests/stressmodel/bench_test.go b/tests/stressmodel/bench_test.go
index 1070f84501..08a87f59f7 100644
--- a/tests/stressmodel/bench_test.go
+++ b/tests/stressmodel/bench_test.go
@@ -75,7 +75,7 @@ func BenchmarkLoad(b *testing.B) {
 func BenchmarkSatisfy(b *testing.B) {
 	for _, n := range networkSizes {
 		src, stats := network(n).Source()
-		b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, stats.Requirements), func(b *testing.B) {
+		b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, stats.Assertions), func(b *testing.B) {
 			sess := loadNetwork(b, src)
 			check := func() {
 				for _, v := range sess.CheckSatisfy("") {
@@ -94,6 +94,75 @@ func BenchmarkSatisfy(b *testing.B) {
 	}
 }
 
+func fleet(satellitesPerPlane int) SatelliteNetwork {
+	n := network(satellitesPerPlane)
+	n.Fleet = true
+	return n
+}
+
+const fleetNetwork = "SatelliteNetwork::Constellation::network"
+
+// BenchmarkFleetInstantiate measures creating the fleet-form network and reading
+// the dry mass of every occurrence in every plane: what it costs to materialize
+// N spacecraft declared as `Spacecraft[N]` and evaluate a summed attribute over
+// each one's component tree.
+func BenchmarkFleetInstantiate(b *testing.B) {
+	for _, n := range networkSizes {
+		src, stats := fleet(n).Source()
+		b.Run(fmt.Sprintf("satellites=%d/elements=%d", stats.Satellites, stats.Elements), func(b *testing.B) {
+			sess := loadNetwork(b, src)
+			read := func() {
+				if _, err := sess.InstantiateNamed(fleetNetwork); err != nil {
+					b.Fatal(err)
+				}
+				for p := 0; p < 4; p++ {
+					if _, err := sess.EvalExpr(fmt.Sprintf("%s.plane%d.sats.dryMass", fleetNetwork, p)); err != nil {
+						b.Fatal(err)
+					}
+				}
+			}
+			read()
+			b.ReportAllocs()
+			b.ResetTimer()
+			for i := 0; i < b.N; i++ {
+				read()
+			}
+			b.StopTimer()
+			b.ReportMetric(float64(b.Elapsed().Nanoseconds())/float64(b.N)/float64(stats.Satellites), "ns/satellite")
+		})
+	}
+}
+
+// BenchmarkFleetSatisfy measures the warm re-check of every satisfy assertion of
+// a fleet-form network: three per block and three per unit stating values of its
+// own, each unit checked as one occurrence of its plane's fleet.
+func BenchmarkFleetSatisfy(b *testing.B) {
+	for _, n := range networkSizes {
+		src, stats := fleet(n).Source()
+		assertions := stats.Assertions
+		b.Run(fmt.Sprintf("satellites=%d/assertions=%d", stats.Satellites, assertions), func(b *testing.B) {
+			sess := loadNetwork(b, src)
+			check := func() {
+				verdicts := sess.CheckSatisfy("")
+				if len(verdicts) != assertions {
+					b.Fatalf("got %d verdicts, want %d", len(verdicts), assertions)
+				}
+				for _, v := range verdicts {
+					if !v.Holds() {
+						b.Fatalf("%s: %v", v.Subject, v.Lines)
+					}
+				}
+			}
+			check()
+			b.ReportAllocs()
+			b.ResetTimer()
+			for i := 0; i < b.N; i++ {
+				check()
+			}
+		})
+	}
+}
+
 // BenchmarkEditBeside measures what an editor pays per keystroke in a small file
 // open beside a network: reparse of the small file, reindex, and diagnostics.
 func BenchmarkEditBeside(b *testing.B) {
diff --git a/tests/stressmodel/satnet.go b/tests/stressmodel/satnet.go
index 4e7a75b0dd..7d53b6e9ed 100644
--- a/tests/stressmodel/satnet.go
+++ b/tests/stressmodel/satnet.go
@@ -8,6 +8,9 @@
 // power budget, the requirements it satisfies and the mode machine it exhibits.
 // Satellites are cross-linked to their neighbours in the same orbital plane and
 // in the adjacent plane, and every satellite has a downlink to a ground station.
+//
+// The network is written either as a `part def` per satellite or, in the fleet
+// form, as `part sats : Block[N]` over a few blocks whose as-built values are defaults.
 package stressmodel
 
 import (
@@ -22,17 +25,39 @@ type SatelliteNetwork struct {
 	Planes, Satellites int
 	// GroundStations is the number of ground stations the constellation downlinks to.
 	GroundStations int
+	// Fleet declares each plane as occurrences of one spacecraft block rather
+	// than one definition per satellite; see the package documentation.
+	Fleet bool
 }
 
+// fleetBlocks is how many spacecraft blocks the fleet form declares; plane p is
+// built from block p mod fleetBlocks.
+const fleetBlocks = 4
+
+// fleetUnitStride is how many satellites of a plane share their block's
+// defaults for each one the fleet form declares as-built values for.
+const fleetUnitStride = 16
+
 // Stats counts what a generated network declares.
 type Stats struct {
+	// Satellites is the number of spacecraft in the constellation, whichever
+	// form declares them; GroundStations the number of ground stations.
 	Satellites, GroundStations int
-	// Components is the number of leaf components across every satellite and station.
+	// Definitions is the number of spacecraft definitions declared: one per
+	// satellite in the single-definition form, one per block in the fleet form.
+	Definitions int
+	// Units is the number of satellites stating as-built values of their own:
+	// every satellite in the single-definition form, the diverging units in the fleet form.
+	Units int
+	// Components is the number of leaf components declared across the spacecraft
+	// definitions, the diverging units and the stations.
 	Components int
 	// Connections is the number of interface usages, inside satellites and between them.
 	Connections int
-	// Requirements is the number of requirement usages, each with a satisfy assertion.
+	// Requirements is the number of requirement usages; Assertions the number of
+	// satisfy assertions, one per requirement plus one per diverging unit in fleet form.
 	Requirements int
+	Assertions   int
 	// Elements is the number of declarations the model makes, library included.
 	Elements int
 	// Bytes is the length of the generated source.
@@ -71,7 +96,11 @@ func (n SatelliteNetwork) Generate(w io.Writer) (Stats, error) {
 	var b strings.Builder
 	g := &generator{b: &b}
 	g.library()
-	g.constellation(n)
+	if n.Fleet {
+		g.fleet(n)
+	} else {
+		g.constellation(n)
+	}
 	g.stats.Bytes = b.Len()
 	_, err := io.WriteString(w, b.String())
 	return g.stats, err
@@ -422,10 +451,22 @@ func (g *generator) link(kind string, a, b int) {
 // satellite writes one fully configured spacecraft definition and its requirements.
 func (g *generator) satellite(id, plane, slot int) {
 	g.stats.Satellites++
+	g.stats.Units++
 	g.decl(2, "part def Sat%d :> Spacecraft {", id)
 	g.decl(3, "attribute :>> catalogId = %d;", 40000+id)
 	g.decl(3, "attribute :>> plane = %d;", plane)
 	g.decl(3, "attribute :>> slot = %d;", slot)
+	g.spacecraftBody(id, "")
+	g.line(2, "}")
+	g.decl(2, "part sat%dConfig : Sat%d;", id, id)
+	g.requirements(fmt.Sprintf("sat%d", id), fmt.Sprintf("sat%dConfig", id), id)
+	g.line(0, "")
+}
+
+// spacecraftBody writes the subsystems, budgets and connections of spacecraft id;
+// valued (`=` or `default =`) writes the values a unit may state its own for.
+func (g *generator) spacecraftBody(id int, valued string) {
+	g.stats.Definitions++
 	var massTerms, powerTerms []string
 	for _, s := range subsystems {
 		massTerms = append(massTerms, s.name+".mass")
@@ -437,10 +478,10 @@ func (g *generator) satellite(id, plane, slot int) {
 			subMass = append(subMass, c.name+".mass")
 			subPower = append(subPower, c.name+".powerDraw")
 			g.redefinePart(4, c.name)
-			g.decl(5, "attribute :>> mass = %d.%d [kg];", 2+(id+j)%40, (id*3+j)%10)
-			g.decl(5, "attribute :>> powerDraw = %d.0 [W];", 5+(id*5+j*7)%50)
-			g.decl(5, "attribute :>> serialNumber = \"%s-%05d-%d\";", strings.ToUpper(c.name), id, j)
-			g.componentDetail(c.def, id, j)
+			g.decl(5, "attribute :>> mass %s= %d.%d [kg];", valued, 2+(id+j)%40, (id*3+j)%10)
+			g.decl(5, "attribute :>> powerDraw %s= %d.0 [W];", valued, 5+(id*5+j*7)%50)
+			g.decl(5, "attribute :>> serialNumber %s= \"%s-%05d-%d\";", valued, strings.ToUpper(c.name), id, j)
+			g.componentDetail(c.def, id, j, valued)
 			g.line(4, "}")
 		}
 		g.decl(4, "attribute :>> mass = %s;", strings.Join(subMass, " + "))
@@ -469,70 +510,202 @@ func (g *generator) satellite(id, plane, slot int) {
 	g.stats.Connections++
 	g.decl(3, "interface payloadToCdh : DataFeed connect payload.dataOut to cdh.dataIn;")
 	g.decl(3, "constraint massMargin { dryMass <= %d [kg] }", 500+id%100)
-	g.line(2, "}")
-	g.decl(2, "part sat%dConfig : Sat%d;", id, id)
+}
+
+// requirements writes the three requirements of the spacecraft configuration
+// named config, with their satisfy assertions, under names prefixed by name.
+func (g *generator) requirements(name, config string, id int) {
 	g.stats.Requirements += 3
-	g.decl(2, "requirement sat%dMass : MassBudget { subject :>> sc = sat%dConfig; attribute :>> limit = %d [kg]; }", id, id, 900+id%100)
+	g.stats.Assertions += 3
+	g.decl(2, "requirement %sMass : MassBudget { subject :>> sc = %s; attribute :>> limit = %d [kg]; }", name, config, 900+id%100)
 	g.stats.Elements += 2
-	g.decl(2, "satisfy sat%dMass by sat%dConfig;", id, id)
-	g.decl(2, "requirement sat%dPower : PowerBudget { subject :>> sc = sat%dConfig; }", id, id)
+	g.decl(2, "satisfy %sMass by %s;", name, config)
+	g.decl(2, "requirement %sPower : PowerBudget { subject :>> sc = %s; }", name, config)
 	g.stats.Elements++
-	g.decl(2, "satisfy sat%dPower by sat%dConfig;", id, id)
-	g.decl(2, "requirement sat%dCrosslink : CrosslinkCapacity { subject :>> sc = sat%dConfig; attribute :>> minimumRate = %d.0; }", id, id, 50+id%50)
+	g.decl(2, "satisfy %sPower by %s;", name, config)
+	g.decl(2, "requirement %sCrosslink : CrosslinkCapacity { subject :>> sc = %s; attribute :>> minimumRate = %d.0; }", name, config, 50+id%50)
 	g.stats.Elements += 2
-	g.decl(2, "satisfy sat%dCrosslink by sat%dConfig;", id, id)
+	g.decl(2, "satisfy %sCrosslink by %s;", name, config)
+}
+
+// fleet writes the constellation as a few spacecraft blocks, each plane as
+// occurrences of one of them, the ground stations and the links between them.
+func (g *generator) fleet(n SatelliteNetwork) {
+	g.decl(1, "package Constellation {")
+	g.line(2, "private import Interfaces::*;")
+	g.line(2, "private import Platform::*;")
+	g.line(2, "private import Requirements::*;")
+	g.line(2, "private import Behavior::*;")
+	g.fleetBody(n)
+	g.line(1, "}")
+	g.line(0, "}")
+}
+
+// fleetBody writes the members of the fleet-form constellation package.
+func (g *generator) fleetBody(n SatelliteNetwork) {
+	blocks := min(fleetBlocks, n.Planes)
+	for b := 0; b < blocks; b++ {
+		g.block(b)
+	}
+	for k := 0; k < n.GroundStations; k++ {
+		g.groundStation(k)
+	}
+	g.decl(2, "part def OrbitalPlane {")
+	g.decl(3, "attribute plane : Integer;")
+	g.decl(3, "part sats : Spacecraft[%d] ordered;", n.Satellites)
+	if n.Satellites > 1 {
+		g.stats.Connections++
+		g.decl(3, "interface ring : RFLink connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx {")
+		g.decl(4, "attribute :>> dataRate = 100.0;")
+		g.decl(4, "attribute :>> slantRange = 2000 [km];")
+		g.line(3, "}")
+	}
+	g.decl(3, "attribute satelliteCount : Integer = %d;", n.Satellites)
+	g.line(2, "}")
 	g.line(0, "")
+	g.decl(2, "part def Network {")
+	for p := 0; p < n.Planes; p++ {
+		g.plane(n, p, p%blocks)
+	}
+	for k := 0; k < n.GroundStations; k++ {
+		g.decl(3, "part gs%d : Station%d;", k, k)
+	}
+	for p := 0; p+1 < n.Planes; p++ {
+		g.stats.Connections++
+		g.decl(3, "interface plane%dTo%d : RFLink connect [1] plane%d.sats.comms.crosslinkTx to [1] plane%d.sats.comms.crosslinkRx {", p, p+1, p, p+1)
+		g.decl(4, "attribute :>> dataRate = %d.0;", 100+(2*p+1)%400)
+		g.decl(4, "attribute :>> slantRange = %d [km];", 2000+(p*10+3)%3000)
+		g.line(3, "}")
+	}
+	for p := 0; p < n.Planes; p++ {
+		for k := 0; k < n.GroundStations; k++ {
+			g.stats.Connections++
+			g.decl(3, "interface downlink%dTo%d : RFLink connect [1] plane%d.sats.comms.rf to [1] gs%d.uplink {", k, p, p, k)
+			g.decl(4, "attribute :>> dataRate = %d.0;", 50+p%200)
+			g.decl(4, "attribute :>> slantRange = %d [km];", 900+p%1500)
+			g.line(3, "}")
+		}
+	}
+	g.decl(3, "attribute satelliteCount : Integer = %d;", n.Planes*n.Satellites)
+	g.line(2, "}")
+	g.decl(2, "part network : Network;")
+	g.line(0, "")
+	for b := 0; b < blocks; b++ {
+		g.decl(2, "part block%sConfig : Block%s;", blockName(b), blockName(b))
+		g.requirements("block"+blockName(b), "block"+blockName(b)+"Config", b)
+	}
+	for p := 0; p < n.Planes; p++ {
+		for s := 0; s < n.Satellites; s += fleetUnitStride {
+			for _, req := range []string{"Mass", "Power", "Crosslink"} {
+				g.stats.Assertions++
+				g.decl(2, "satisfy block%s%s by network.plane%d.unit%d;", blockName(p%blocks), req, p, s)
+			}
+		}
+	}
+}
+
+// block writes one spacecraft block: a definition whose as-built values are
+// defaults, so a unit built from it states only the values it diverges in.
+func (g *generator) block(b int) {
+	g.decl(2, "part def Block%s :> Spacecraft {", blockName(b))
+	g.decl(3, "attribute :>> catalogId default = %d;", 40000+b*10000)
+	g.decl(3, "attribute :>> slot default = 0;")
+	g.spacecraftBody(b, "default ")
+	g.line(2, "}")
+	g.line(0, "")
+}
+
+// plane writes orbital plane p as occurrences of block b, the units diverging
+// from the block stating their catalog identity, slot and as-built terminal.
+func (g *generator) plane(n SatelliteNetwork, p, b int) {
+	g.decl(3, "part plane%d : OrbitalPlane {", p)
+	g.decl(4, "attribute :>> plane = %d;", p)
+	g.decl(4, "part :>> sats : Block%s { attribute :>> plane = %d; }", blockName(b), p)
+	g.stats.Elements++
+	for s := 0; s < n.Satellites; s++ {
+		g.stats.Satellites++
+		if s%fleetUnitStride != 0 {
+			continue
+		}
+		id := p*n.Satellites + s
+		g.stats.Units++
+		g.stats.Components++
+		g.decl(4, "part unit%d :> sats {", s)
+		g.decl(5, "attribute :>> catalogId = %d;", 40000+id)
+		g.decl(5, "attribute :>> slot = %d;", s)
+		g.decl(5, "part :>> comms {")
+		g.decl(6, "part :>> crosslinkTerminal {")
+		g.decl(7, "attribute :>> mass = %d.%d [kg];", 2+(id+1)%40, (id*3+1)%10)
+		g.decl(7, "attribute :>> serialNumber = \"CROSSLINKTERMINAL-%05d-1\";", id)
+		g.decl(7, "attribute :>> dataRate = %s;", crosslinkDataRate(id))
+		g.line(6, "}")
+		g.line(5, "}")
+		g.line(4, "}")
+	}
+	g.line(3, "}")
+}
+
+// blockName letters the spacecraft blocks A, B, C, ...
+func blockName(b int) string {
+	return string(rune('A' + b))
+}
+
+// crosslinkDataRate is the as-built data rate of the crosslink terminal of the
+// spacecraft or block numbered id.
+func crosslinkDataRate(id int) string {
+	return fmt.Sprintf("%d.0", 100+(id*3)%400)
 }
 
-// componentDetail writes the as-built values of the attributes a component kind adds.
-func (g *generator) componentDetail(def string, id, j int) {
+// componentDetail writes the as-built values of the attributes a component kind
+// adds, each valued with the given keyword ("default " or none).
+func (g *generator) componentDetail(def string, id, j int, valued string) {
 	switch def {
 	case "SolarArray":
-		g.decl(5, "attribute :>> area = %d.%d ['m²'];", 4+id%6, id%10)
-		g.decl(5, "attribute :>> generated = %d.0 [W];", 1200+(id*13)%700)
+		g.decl(5, "attribute :>> area %s= %d.%d ['m²'];", valued, 4+id%6, id%10)
+		g.decl(5, "attribute :>> generated %s= %d.0 [W];", valued, 1200+(id*13)%700)
 	case "Battery":
-		g.decl(5, "attribute :>> capacity = %d.0 [J];", 3600000+(id*17)%7200000)
-		g.decl(5, "attribute :>> depthOfDischarge = 0.%d;", 2+id%5)
+		g.decl(5, "attribute :>> capacity %s= %d.0 [J];", valued, 3600000+(id*17)%7200000)
+		g.decl(5, "attribute :>> depthOfDischarge %s= 0.%d;", valued, 2+id%5)
 	case "PowerConditioner":
-		g.decl(5, "attribute :>> efficiency = 0.9%d;", id%10)
+		g.decl(5, "attribute :>> efficiency %s= 0.9%d;", valued, id%10)
 	case "StarTracker":
-		g.decl(5, "attribute :>> accuracy = %d.0 [arcsec];", 1+id%5)
-		g.decl(5, "attribute :>> updateRate = %d.0 [Hz];", 2+id%8)
+		g.decl(5, "attribute :>> accuracy %s= %d.0 [arcsec];", valued, 1+id%5)
+		g.decl(5, "attribute :>> updateRate %s= %d.0 [Hz];", valued, 2+id%8)
 	case "InertialMeasurementUnit":
-		g.decl(5, "attribute :>> driftRate = 0.0%d;", 1+id%9)
+		g.decl(5, "attribute :>> driftRate %s= 0.0%d;", valued, 1+id%9)
 	case "ReactionWheel":
-		g.decl(5, "attribute :>> maxTorque = 0.%d ['N⋅m'];", 1+(id+j)%9)
-		g.decl(5, "attribute :>> momentumCapacity = %d.0;", 10+(id+j)%40)
+		g.decl(5, "attribute :>> maxTorque %s= 0.%d ['N⋅m'];", valued, 1+(id+j)%9)
+		g.decl(5, "attribute :>> momentumCapacity %s= %d.0;", valued, 10+(id+j)%40)
 	case "OnboardComputer":
-		g.decl(5, "attribute :>> clockRate = %d.0 [Hz];", 200000000+(id*11)%600000000)
-		g.decl(5, "attribute :>> memoryBytes = %d;", (1+id%8)*1073741824)
+		g.decl(5, "attribute :>> clockRate %s= %d.0 [Hz];", valued, 200000000+(id*11)%600000000)
+		g.decl(5, "attribute :>> memoryBytes %s= %d;", valued, (1+id%8)*1073741824)
 	case "MassMemory":
-		g.decl(5, "attribute :>> capacityBytes = %d;", (16+id%48)*1073741824)
+		g.decl(5, "attribute :>> capacityBytes %s= %d;", valued, (16+id%48)*1073741824)
 	case "Transponder":
-		g.decl(5, "attribute :>> frequency = %d.0 [Hz];", 8000000000+(id*7)%400000000)
-		g.decl(5, "attribute :>> transmitPower = %d.0 [W];", 10+id%40)
+		g.decl(5, "attribute :>> frequency %s= %d.0 [Hz];", valued, 8000000000+(id*7)%400000000)
+		g.decl(5, "attribute :>> transmitPower %s= %d.0 [W];", valued, 10+id%40)
 	case "CrosslinkTerminal":
-		g.decl(5, "attribute :>> wavelength = 1550 [nm];")
-		g.dataRate(5, 100+(id*3)%400)
+		g.decl(5, "attribute :>> wavelength %s= 1550 [nm];", valued)
+		g.decl(5, "attribute :>> dataRate %s= %s;", valued, crosslinkDataRate(id))
 	case "Antenna":
-		g.decl(5, "attribute :>> gain = %d.%d;", 20+id%20, id%10)
-		g.decl(5, "attribute :>> diameter = 0.%d [m];", 3+id%6)
+		g.decl(5, "attribute :>> gain %s= %d.%d;", valued, 20+id%20, id%10)
+		g.decl(5, "attribute :>> diameter %s= 0.%d [m];", valued, 3+id%6)
 	case "PropellantTank":
-		g.decl(5, "attribute :>> propellantMass = %d.0 [kg];", 30+(id*5)%100)
-		g.decl(5, "attribute :>> volume = 0.%d ['m³'];", 1+id%5)
+		g.decl(5, "attribute :>> propellantMass %s= %d.0 [kg];", valued, 30+(id*5)%100)
+		g.decl(5, "attribute :>> volume %s= 0.%d ['m³'];", valued, 1+id%5)
 	case "Thruster":
-		g.decl(5, "attribute :>> thrust = %d.0 [mN];", 20+id%200)
-		g.decl(5, "attribute :>> specificImpulse = %d.0 [s];", 1200+(id*19)%800)
+		g.decl(5, "attribute :>> thrust %s= %d.0 [mN];", valued, 20+id%200)
+		g.decl(5, "attribute :>> specificImpulse %s= %d.0 [s];", valued, 1200+(id*19)%800)
 	case "Radiator":
-		g.decl(5, "attribute :>> area = 1.%d ['m²'];", id%10)
-		g.decl(5, "attribute :>> emissivity = 0.8%d;", id%10)
+		g.decl(5, "attribute :>> area %s= 1.%d ['m²'];", valued, id%10)
+		g.decl(5, "attribute :>> emissivity %s= 0.8%d;", valued, id%10)
 	case "Heater":
-		g.decl(5, "attribute :>> setpoint = %d.0 [K];", 283+id%20)
+		g.decl(5, "attribute :>> setpoint %s= %d.0 [K];", valued, 283+id%20)
 	case "ImagingSensor":
-		g.decl(5, "attribute :>> groundSampleDistance = 0.%d [m];", 3+id%7)
-		g.decl(5, "attribute :>> swath = %d.0 [km];", 10+id%30)
+		g.decl(5, "attribute :>> groundSampleDistance %s= 0.%d [m];", valued, 3+id%7)
+		g.decl(5, "attribute :>> swath %s= %d.0 [km];", valued, 10+id%30)
 	case "PayloadProcessor":
-		g.decl(5, "attribute :>> throughput = %d.0;", 100+(id*23)%900)
+		g.decl(5, "attribute :>> throughput %s= %d.0;", valued, 100+(id*23)%900)
 	}
 }
 
@@ -549,7 +722,7 @@ func (g *generator) groundStation(k int) {
 		g.decl(4, "attribute :>> mass = %d.0 [kg];", 50+(k*7+j*11)%900)
 		g.decl(4, "attribute :>> powerDraw = %d.0 [W];", 100+(k*13+j*17)%2000)
 		g.decl(4, "attribute :>> serialNumber = \"GS-%s-%03d\";", strings.ToUpper(c.name), k)
-		g.componentDetail(c.def, k, j)
+		g.componentDetail(c.def, k, j, "")
 		g.line(3, "}")
 	}
 	g.line(2, "}")
diff --git a/tests/stressmodel/satnet_test.go b/tests/stressmodel/satnet_test.go
index aa4326c99e..746def2059 100644
--- a/tests/stressmodel/satnet_test.go
+++ b/tests/stressmodel/satnet_test.go
@@ -18,8 +18,8 @@ func TestSatelliteNetworkValidates(t *testing.T) {
 	if stats.Satellites != 4 || stats.GroundStations != 1 {
 		t.Fatalf("stats = %+v, want 4 satellites and 1 station", stats)
 	}
-	if stats.Requirements != 3*stats.Satellites {
-		t.Errorf("Requirements = %d, want three per satellite", stats.Requirements)
+	if stats.Requirements != 3*stats.Satellites || stats.Assertions != stats.Requirements {
+		t.Errorf("Requirements = %d, Assertions = %d, want three per satellite", stats.Requirements, stats.Assertions)
 	}
 	if stats.Bytes != len(src) {
 		t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src))
@@ -31,8 +31,8 @@ func TestSatelliteNetworkValidates(t *testing.T) {
 		t.Errorf("diagnostic: %s", d.Message)
 	}
 	verdicts := s.CheckSatisfy("")
-	if len(verdicts) != stats.Requirements {
-		t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Requirements)
+	if len(verdicts) != stats.Assertions {
+		t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Assertions)
 	}
 	for _, v := range verdicts {
 		if !v.Holds() {
@@ -61,6 +61,99 @@ func TestSatelliteNetworkScales(t *testing.T) {
 	}
 }
 
+// TestFleetValidates keeps the fleet form in step with the grammar and the
+// runtime: a constellation of a few blocks with occurrence counts loads under
+// strict conformance without a diagnostic, its satisfy assertions hold, and the
+// occurrences read the block's defaults where a unit states nothing of its own.
+func TestFleetValidates(t *testing.T) {
+	n := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true}
+	src, stats := n.Source()
+	if stats.Satellites != 4*fleetUnitStride || stats.GroundStations != 1 {
+		t.Fatalf("stats = %+v, want %d satellites and 1 station", stats, 4*fleetUnitStride)
+	}
+	if stats.Definitions != 2 || stats.Units != 4 {
+		t.Errorf("stats = %+v, want 2 blocks and 4 diverging units", stats)
+	}
+	if stats.Requirements != 3*stats.Definitions || stats.Assertions != 3*(stats.Definitions+stats.Units) {
+		t.Errorf("Requirements = %d, Assertions = %d, want three per block and three more per unit", stats.Requirements, stats.Assertions)
+	}
+	if stats.Bytes != len(src) {
+		t.Errorf("Bytes = %d, want %d", stats.Bytes, len(src))
+	}
+	for _, want := range []string{
+		"attribute :>> dataRate default = ",
+		"attribute :>> area default = ",
+		"connect [1] sats.comms.crosslinkTx to [1] sats.comms.crosslinkRx",
+		"connect [1] plane0.sats.comms.crosslinkTx to [1] plane1.sats.comms.crosslinkRx",
+	} {
+		if !strings.Contains(src, want) {
+			t.Errorf("source lacks %q", want)
+		}
+	}
+
+	s := repl.NewSession()
+	s.SetConformanceMode(diag.ConformanceModeOf(true))
+	for _, d := range s.Submit(src).Diagnostics {
+		t.Errorf("diagnostic: %s", d.Message)
+	}
+	verdicts := s.CheckSatisfy("")
+	if want := stats.Assertions; len(verdicts) != want {
+		t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), want)
+	}
+	for _, v := range verdicts {
+		if !v.Holds() {
+			t.Errorf("%s: %v", v.Subject, v.Lines)
+		}
+	}
+
+	const network = "SatelliteNetwork::Constellation::network"
+	for expr, want := range map[string]string{
+		network + ".plane1.sats#(1).catalogId":                          "= 40032",
+		network + ".plane1.sats#(2).slot":                               "= 16",
+		network + ".plane1.sats#(3).catalogId":                          "= 50000",
+		network + ".plane1.unit0.catalogId":                             "= 40032",
+		network + ".plane1.unit16.comms.crosslinkTerminal.serialNumber": `= "CROSSLINKTERMINAL-00048-1"`,
+		network + ".plane1.unit16.comms.crosslinkTerminal.dataRate":     "= 244.0",
+		network + ".plane1.sats#(3).comms.crosslinkTerminal.dataRate":   "= 103.0",
+		network + ".plane1.sats#(3).eps.solarArray.area":                "= 5.1 ['m²']",
+		network + ".plane0.sats#(3).plane":                              "= 0",
+		network + ".satelliteCount":                                     "= 64",
+	} {
+		lines, err := s.EvalExpr(expr)
+		if err != nil {
+			t.Errorf("%s: %v", expr, err)
+			continue
+		}
+		if got := strings.TrimSpace(lines[len(lines)-1]); got != want {
+			t.Errorf("%s = %q, want %q", expr, got, want)
+		}
+	}
+}
+
+// TestFleetScales checks the fleet form declares the blocks, the planes and the
+// links but not the satellites: the element count grows with the planes and the
+// diverging units, not with the occurrences.
+func TestFleetScales(t *testing.T) {
+	_, small := SatelliteNetwork{Planes: 2, Satellites: fleetUnitStride, GroundStations: 1, Fleet: true}.Source()
+	_, wide := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true}.Source()
+	_, wider := SatelliteNetwork{Planes: 2, Satellites: 8 * fleetUnitStride, GroundStations: 1, Fleet: true}.Source()
+	_, tall := SatelliteNetwork{Planes: 4, Satellites: fleetUnitStride, GroundStations: 1, Fleet: true}.Source()
+	_, legacy := SatelliteNetwork{Planes: 2, Satellites: fleetUnitStride, GroundStations: 1}.Source()
+	if wider.Satellites != 8*small.Satellites || wider.Definitions != small.Definitions {
+		t.Errorf("more satellites per plane changed the blocks: %+v vs %+v", wider, small)
+	}
+	perUnit := wide.Elements - small.Elements
+	if wide.Units-small.Units != 2 || wider.Units != 8*small.Units || wider.Elements-small.Elements != (wider.Units-small.Units)*perUnit/2 {
+		t.Errorf("elements do not grow only with the diverging units: %+v, %+v vs %+v", wider, wide, small)
+	}
+	if tall.Definitions != 4 || tall.Connections <= small.Connections {
+		t.Errorf("more planes add no blocks or links: %+v vs %+v", tall, small)
+	}
+	if legacy.Satellites != small.Satellites || legacy.Elements <= 4*small.Elements {
+		t.Errorf("the fleet form is not much smaller than one definition per satellite: %+v vs %+v", small, legacy)
+	}
+}
+
 // splitFiles is a network split by plane as the CLI loads it, one source per file.
 func splitFiles(n SatelliteNetwork) ([]repl.SourceFile, Stats) {
 	files, stats := n.Split()
@@ -118,9 +211,33 @@ func TestSatelliteNetworkFilesValidate(t *testing.T) {
 		t.Fatalf("got %d files, want the library, %d planes and the network", len(files), n.Planes)
 	}
 	_, whole := n.Source()
-	if stats.Satellites != whole.Satellites || stats.Requirements != whole.Requirements || stats.Connections != whole.Connections {
+	if stats.Satellites != whole.Satellites || stats.Assertions != whole.Assertions || stats.Connections != whole.Connections {
+		t.Fatalf("split stats %+v, single-file stats %+v", stats, whole)
+	}
+	validateFiles(t, files, stats.Assertions)
+}
+
+// TestFleetFilesValidate keeps the split fleet form in step with the whole one:
+// the library and the constellation as two documents declare the same network,
+// load clean under strict conformance, and hold every satisfy assertion.
+func TestFleetFilesValidate(t *testing.T) {
+	n := SatelliteNetwork{Planes: 2, Satellites: 2 * fleetUnitStride, GroundStations: 1, Fleet: true}
+	files, stats := n.Split()
+	if len(files) != 2 {
+		t.Fatalf("got %d files, want the library and the constellation", len(files))
+	}
+	_, whole := n.Source()
+	if stats.Elements != whole.Elements || stats.Definitions != whole.Definitions || stats.Units != whole.Units ||
+		stats.Satellites != whole.Satellites || stats.Assertions != whole.Assertions || stats.Connections != whole.Connections {
 		t.Fatalf("split stats %+v, single-file stats %+v", stats, whole)
 	}
+	validateFiles(t, files, stats.Assertions)
+}
+
+// validateFiles opens files as one workspace and one session, wanting no
+// diagnostic and the given number of satisfy assertions, all holding.
+func validateFiles(t *testing.T, files []File, assertions int) {
+	t.Helper()
 	ws := model.NewWorkspace(model.WithConformanceMode(diag.ConformanceModeOf(true)))
 	for _, f := range files {
 		ws.Open(f.Name, []byte(f.Source), 1)
@@ -141,8 +258,8 @@ func TestSatelliteNetworkFilesValidate(t *testing.T) {
 		t.Errorf("diagnostic: %s", d.Message)
 	}
 	verdicts := s.CheckSatisfy("")
-	if len(verdicts) != stats.Requirements {
-		t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), stats.Requirements)
+	if len(verdicts) != assertions {
+		t.Fatalf("got %d satisfy verdicts, want %d", len(verdicts), assertions)
 	}
 	for _, v := range verdicts {
 		if !v.Holds() {
diff --git a/tests/stressmodel/split.go b/tests/stressmodel/split.go
index 658341eae4..51add371ef 100644
--- a/tests/stressmodel/split.go
+++ b/tests/stressmodel/split.go
@@ -13,6 +13,8 @@ type File struct {
 // Split generates the network Generate writes as one document per orbital plane
 // beside the shared library and the constellation joining the planes. Each plane
 // imports the library by qualified name, so a file resolves against the others.
+// The fleet form declares its planes inside the network, so it splits into the
+// library and the constellation alone.
 func (n SatelliteNetwork) Split() ([]File, Stats) {
 	var b strings.Builder
 	g := &generator{b: &b}
@@ -28,6 +30,15 @@ func (n SatelliteNetwork) Split() ([]File, Stats) {
 	g.line(0, "}")
 	files = append(files, take("library.sysml"))
 
+	if n.Fleet {
+		g.decl(0, "package Constellation {")
+		g.planeImports()
+		g.line(0, "")
+		g.fleetBody(n)
+		g.line(0, "}")
+		return append(files, take("constellation.sysml")), g.stats
+	}
+
 	id := 0
 	for p := 0; p < n.Planes; p++ {
 		g.decl(0, "package Plane%d {", p)
diff --git a/tools/cmd/stress-model/main.go b/tools/cmd/stress-model/main.go
index b89aee40ac..5d6f407c79 100644
--- a/tools/cmd/stress-model/main.go
+++ b/tools/cmd/stress-model/main.go
@@ -1,5 +1,7 @@
 // Command stress-model writes a large generated satellite-network model to stdout,
-// or one file per orbital plane; see docs/project/satellite-network-stress-test.md.
+// or one file per orbital plane, with one definition per satellite or, with -fleet,
+// as occurrences of a few spacecraft blocks. See docs/project/satellite-network-stress-test.md
+// and docs/guide/modeling-fleets.md.
 package main
 
 import (
@@ -20,6 +22,7 @@ func main() {
 	planes := flag.Int("planes", 4, "orbital planes in the constellation")
 	perPlane := flag.Int("satellites", 8, "satellites in each orbital plane")
 	stations := flag.Int("ground-stations", 3, "ground stations the constellation downlinks to")
+	fleet := flag.Bool("fleet", false, "declare each plane as occurrences of one spacecraft block rather than one definition per satellite")
 	stats := flag.Bool("stats", false, "report on stderr what the model declares")
 	split := flag.String("split-planes", "", "write one .sysml per orbital plane, beside the library and the constellation, into this directory instead of stdout")
 	flag.Parse()
@@ -31,7 +34,7 @@ func main() {
 		fmt.Fprintln(os.Stderr, "stress-model: -planes and -satellites must be at least 1 and -ground-stations at least 0")
 		os.Exit(2)
 	}
-	n := stressmodel.SatelliteNetwork{Planes: *planes, Satellites: *perPlane, GroundStations: *stations}
+	n := stressmodel.SatelliteNetwork{Planes: *planes, Satellites: *perPlane, GroundStations: *stations, Fleet: *fleet}
 	var (
 		s   stressmodel.Stats
 		err error
@@ -46,8 +49,8 @@ func main() {
 		os.Exit(1)
 	}
 	if *stats {
-		fmt.Fprintf(os.Stderr, "satellites=%d ground-stations=%d components=%d connections=%d requirements=%d elements=%d bytes=%d\n",
-			s.Satellites, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Elements, s.Bytes)
+		fmt.Fprintf(os.Stderr, "satellites=%d definitions=%d units=%d ground-stations=%d components=%d connections=%d requirements=%d assertions=%d elements=%d bytes=%d\n",
+			s.Satellites, s.Definitions, s.Units, s.GroundStations, s.Components, s.Connections, s.Requirements, s.Assertions, s.Elements, s.Bytes)
 	}
 }