The design for generated executable specs — the third artifact of the transpile output (Reference §22, "The extension framework"): alongside the runtime surface, the transpiler emits tests derived from the Velle spec, organized so a human can find the use case. The philosophy this serves: reading code is the hardest problem in software; Velle surfaces what matters — the spec, and readable, well-organized executable specs that verify it — and pushes generated code down. A human reads the .velle file and these specs to understand the system; the code below them is scoped to a function at a time.

The unit a human searches for is a state and what reacts to it — a refinement plus the rules hanging off it. One generated spec file per story root:

• A rule files under its condition's story root. The root is computed by walking the condition: a composition takes its leftmost operand (ActionableOverdue → OverdueInvoice); a partition refinement over an act shape whose predicate tests membership in another refinement roots there (ApplicableDueChange → IssuedInvoice — the freeze's story); a chain rule whose trigger shape is produced (not an act), roots with its producer (EmailReceipt → UnemailedReceipt → Receipt ← produced by SendReceipt → PaidInvoice).
• prohibitions (never, requires) and act-triggered rules file under their act shape.
• Every file opens with the Velle it verifies, quoted verbatim (pretty-printed from the AST) — reading the spec file is reading the description plus its proof.
• A generated SPEC_INDEX-<System>.md per system lists every file and every case sentence: the table of contents for "what does this system do." Each system's generated output lives in its own package (velle.generated.<system> / .specs) inside its own output module (examples/<system>/output/).
• The same cases are also rendered as Gherkin, one features/<system>/<Root>.feature per story root — documentation, not a runner: JUnit stays the execution engine, and the feature files are regenerated from the same AST in the same pass, so they can't drift from what actually runs. Cucumber's sentence-matching machinery exists to keep hand-written prose and hand-written glue in sync; generation from one source already provides that guarantee, so executing the sentences would add indirection and buy nothing.

Construct	Generated cases
Entry rule	the entering commit produces the effects; produced facts link back (field: this ⇒ field == subject); assignment values land (invoice.due = newDue ⇒ readable equality)
Guarded / after commit rule	firing happened after the boundary; the disarm holds (subject left its trigger state); backstop ticks are harmless (counts stable)
Tick sweep	member at tick → effect + linkage; the guard holds across ticks; a literal time window (today - 7 days) is advanced past and the sweep reopens
when leaving rule	exit produces the effects; the subject is no longer a member
Partition pair	the act subject is a member of exactly one side
never or requires (single comparison against a literal, on an act)	a violating act is refused and nothing commits; a boundary-legal act is accepted; the case titles follow the author's spelling

Generated cases need scenario data the spec doesn't contain — which commits reach the interesting state is human judgment. The contract:

• The generator derives the whens and thens. Effects, linkage, disarm, refusals, windows — everything above is mechanical.
• The developer owes the givens — and the generator demands them by name. It emits a RequiredGivens interface, one documented method per scenario the spec's cases require, returning the subject as a typed view. Names are scenario language derived from the condition, not the rule: a bare condition names the state itself (paidInvoice(): BillingSystem.InvoiceView, unappliedDeposit()), and rules sharing that condition share the one given; a condition carrying an inline where (or a composite) can't be named, so the rule disambiguates (memberForRestoreService()). An exit rule's test performs the "when" itself and asserts both sides of the transition; the exit commit is derived when the predicate names it — a not exists X for this atom over an act means the test commits the real X (sys.commitReopenTicket(ticket)), no given owed — and only a drift exit (a value predicate like balance < 0) demands a human-owned exit action beside the state-given (delinquent() / exitDelinquent(member)), since which commit recovers the value is business judgment. An act declared by is committed by someone (Reference §22, "The actor"), so a derived commit demands a given for the actor too — someStaff(), or someAdministrator() when the header names the role — and passes it beside the input (sys.commit(NewVerifyFill(fill, ...), actor)); the role gate the header states is not synthesized into a refusal case, since its subject is the actor and not a field. The developer implements it as class Givens(sys) beside the generated specs; a missing given is a compile error naming exactly what's owed. Human judgment stays, but in one findable place, named in business language.
• Each test states its given in place. The call site carries a // given: ... comment describing the state the given has delivered ("a former member of 'ClosedTicket' — the exit commit has just landed"), so a test reads as a self-contained given/when/then without leaving the file.
• Generated tests sanity-check the givens (the returned subject must actually be a member of the condition) so a wrong given fails loudly, not silently.

1. (built) Story-root organization, provenance headers, the case catalog above, RequiredGivens demanding, SPEC_INDEX.md.
2. Boundary-value synthesis for refinement membership (predicate-driven value solving beyond single-literal comparisons); "already a member doesn't re-fire" cases; a scenario DSL (given/whenCommitted/then with entered/produced/refusedBecause vocabulary) replacing plain assertions; fold value assertions via the evaluator.
3. The example construct: the spec itself carries named example instances, collapsing the human-givens tier into full derivation — the description becomes self-illustrating (Reference §22).