diff --git a/docs/testing.md b/docs/testing.md
index a37c665..07ec095 100644
--- a/docs/testing.md
+++ b/docs/testing.md
@@ -2917,6 +2917,71 @@ span (acquisition through as-of, 0.00 where the schedule reaches no month)
 and every `answer_*` figure against the loader's same check (the two must
 agree on all 56 examples).
 
+## P13 steps 4 and 5: the specification text, the laws, the derivation, GnuCash (2026-10-29)
+
+Step 4 writes the first edition (`bookspec/spec/*.md`, 667 lines of the 3,300
+its 60 pages allow), puts the five laws in Lean (`bookspec/lean`, ported from
+`verify/lean`: debits equal credits, the accounting equation, the trial
+balance balances, net income articulates to equity, the cash-flow sections
+sum to the change in cash) and adds eight examples for the laws that had
+none (`entry-an-unbalanced-entry-is-refused`,
+`entry-a-line-amount-is-positive`, `entry-cents-add-exactly`,
+`ledger-a-fraction-of-a-cent-is-refused`,
+`ledger-a-child-account-has-its-parents-type`,
+`ledger-a-mistake-is-reversed-never-erased`,
+`statement-the-books-balance-and-the-equation-holds`,
+`period-a-close-sweeps-the-year-into-capital`); every figure is worked by
+hand in the file and the adapter checks the engine against it. Step 5 adds
+the checker's own derivation (`bookspec/checker/src/derive.rs`) and GnuCash
+as a second engine (`bookspec/gnucash`). Not done: step 6 (the repository of
+its own), and the examples for rules whose events or queries the schema does
+not have (BS-entry-4, BS-ledger-7, -9, -12, BS-asset-2, -3, BS-revenue-1,
+BS-arap-1, -6, BS-format-1); each says so in its section.
+
+- **`bookspec/checker` `tests/spec.rs`:** `every_rule_has_its_section` (45
+  sections, in the file of their area, headed with the B-number),
+  `every_stated_rule_is_complete` (status agrees with the catalogue, MUST /
+  SHOULD / MAY, a symbolic form, applicability; a reserved rule says so),
+  `the_examples_are_the_catalogues` (a section lists exactly the catalogue's
+  examples; "none yet" says why), `every_citation_resolves` (every vendored
+  source exists and every quoted pin is verbatim in it, after whitespace and
+  typographic quotes; an external reference is exact), `the_edition_fits_its_page_budget`,
+  `rules_without_examples_are_not_claimable`.
+- **`bookspec/checker` `tests/lean.rs`:** `the_five_laws_are_stated_and_audited`
+  (no `sorry`), `the_laws_use_standard_axioms_only` (runs `lake build` and
+  `lake env lean Audit.lean` when Lean is installed; skips with a message
+  otherwise).
+- **`bookspec/checker` `tests/derive.rs`:** `no_example_disagrees_with_its_derivation`,
+  `the_law_examples_are_derived_in_full` (no skipped result),
+  `a_wrong_expectation_is_caught` (one cent moved; a refusal the rules do not
+  justify).
+- **`bookspec/gnucash` `tests/gnucash.rs`** (ignored: needs Docker and the
+  image `just oracle` builds; run with `cargo test -p bookspec-gnucash --
+  --ignored`): `gnucash_differs_only_where_it_was_adjudicated` (the three
+  differences, no others, and BS-entry-3, BS-ledger-3, BS-statement-1 and
+  BS-statement-2 pass) and
+  `what_gnucash_did_with_the_entries_the_specification_refuses` (the
+  evidence: ten dollars and 200.00 parked in an Imbalance account, 10.005
+  rounded to 10.01).
+- **`ledger-core` `tests/bookspec.rs`:** `every_bookspec_example_holds` and
+  `the_runner_reports_every_claimed_rule_green`, unchanged in what they
+  prove, now over 66 examples; `BS-entry-1` to `BS-entry-3`, `BS-ledger-1` to
+  `-6`, `BS-ledger-8`, `BS-statement-1`, `-2`, `BS-period-1` and `-2` are now
+  claimed. The adapter's `refusal` maps eight more engine errors to the
+  examples' words.
+
+**For P12 (mutation targets, none run, D-33):** the adapter's `refusal` arms
+(`UnbalancedEntry`, `NegativeAmountLine`, `ZeroAmountLine`,
+`FinerThanMinorUnit`, `ParentTypeMismatch`, `EntryAlreadyReversed`,
+`ClosedPeriod`), each pinned by the example that expects it, and the
+`money` closure's positivity test for an accepted entry; `rule_for_refusal`'s
+new arms; `schema::check_amount`'s `positive` flag for a refused entry;
+`derive`'s `refusal_justified` arms (each reason against its symbolic
+condition), `Model::post`'s close (a debit-normal balance credits, the
+equity line's sign), `signed`'s date window and `closings` flag, and the
+accounting-equation check; the spec test's pin search (a mutant that skips
+the quote check passes only if `every_citation_resolves` has no bad pin).
+
 ## U0b: one attention engine over `PackageBooks` (2026-10-26)
 
 Needs attention moved out of the viewer into `ledger-package::attention`
diff --git a/plan/served.md b/plan/served.md
index 850fd1d..974ea0a 100644
--- a/plan/served.md
+++ b/plan/served.md
@@ -1640,7 +1640,15 @@ Each unit follows the 8.0.4 template. "A-n" is an owner answer numbered in 8.3.1
 5. **Files:** owns `bookspec/**`; touches `crates/ledger-core/tests/bookspec.rs`, `crates/ledger-package/tests/package.rs`, `docs/spec/rules.md` (ids), `Cargo.toml` (workspace members if the checker joins the workspace).
 6. **Tests and proofs:** `every_bookspec_example_holds` unchanged; `bookspec/checker` tests (the schema, the derivations); `bookspec/lean` builds with standard axioms only.
 7. **Done when:** (1) the checker crate exists and `just check` still checks all 56+ examples; (2) the `Engine` trait and the wanderbooks adapter run the runner green for every claimed rule; (3) every B-rule has an id, statement, source and example; (4) the five laws are theorems in `bookspec/lean`; (5) the GnuCash adapter runs and its differences are settled from the sources (recorded in the As-built block).
-8. **As built:** none yet.
+8. **As built:** steps 1-3 landed 2026-10-26 (`579d0eed`); steps 4 and 5 built 2026-10-29 on branch `P13` (step 6 not started: it waits on the owner, see below).
+   - **Step 4, the text.** `bookspec/spec/` holds `00-model.md` (definitions, the model, the five laws, how an example is checked) and one file per area (`entry`, `ledger`, `statement`, `period`, `partner`, `asset`, `prepaid`, `revenue`, `arap`, `1099`, `format`), 667 lines of the 3,300 a 60-page edition allows. Every B-rule has a section `### BS-<area>-<n> (B-n)` with status, MUST/SHOULD/MAY statement, sources, symbolic form, examples and applicability; B-39, B-40, B-43, B-45 are reserved sections (allocated, not yet stated in `rules.md`); B-44, stated in `rules.md`, now carries its `bookspec:` line and CONVENTION status (catalogue and index updated). `checker/tests/spec.rs` fails the build on a missing section, a statement without a modal verb, a status that differs from the catalogue, examples that differ from the catalogue, a vendored pin that is not verbatim in its source (whitespace and curly quotes normalized), or more than 60 pages.
+   - **The five laws** are Lean theorems `Bookspec.law_debits_equal_credits`, `law_accounting_equation`, `law_trial_balance`, `law_net_income_articulates`, `law_cash_flow_is_change_in_cash` in `bookspec/lean` (Basic, Entry, Statements, Closing, Ledger ported from `verify/lean` under the namespace `Bookspec`; `Laws.lean` states them; `Audit.lean` prints their axioms: `propext`, `Quot.sound`, `Classical.choice` only). `checker/tests/lean.rs` builds and audits when Lean is installed.
+   - **New examples (8)**, each figure worked by hand in the file: `entry-an-unbalanced-entry-is-refused`, `entry-a-line-amount-is-positive`, `entry-cents-add-exactly`, `ledger-a-fraction-of-a-cent-is-refused`, `ledger-a-child-account-has-its-parents-type`, `ledger-a-mistake-is-reversed-never-erased`, `statement-the-books-balance-and-the-equation-holds`, `period-a-close-sweeps-the-year-into-capital` (66 in all). Rules now with an example: B-1 to B-12 and B-21, B-23 (`arap-hand-control-posting-refused` also shows it). New refusal words: `unbalanced`, `too_few_lines`, `negative_amount`, `zero_amount`, `finer_than_minor_unit`, `parent_type_mismatch`, `already_reversed`, `period_closed`; a refused entry may carry a non-positive amount. Finding while writing: `close ... to = "retained_earnings"` posts to the role account 3999 Retained Earnings, not to a setup capital account; the example says so.
+   - **Step 5, the derivation.** `bookspec/checker/src/derive.rs` is an engine-free reference model (exact decimals) that replays entries, reversals, a close to retained earnings, bills and invoices, derives `trial_balance`, `balances`, `profit_and_loss` and `entry` figures plus the law checks (books net to zero, A = L + E + (R - X)) and checks each refusal against its rule; everything else is reported `Skipped`, never passed. `checker/tests/derive.rs`: no example disagrees; the eight law examples are derived in full; a figure moved by a cent and an unjustified refusal are both caught.
+   - **The runner against wanderbooks** (`the_runner_reports_every_claimed_rule_green`) is green for every claimed rule, now including BS-entry-1 to -3, BS-ledger-1 to -6 and -8, BS-statement-1 and -2, BS-period-1 and -2.
+   - **GnuCash, the second engine** (`bookspec/gnucash`, ignored tests; needs the `just oracle` image). It claims the rules whose examples ask only for balances. Passes BS-entry-3, BS-ledger-3, BS-statement-1, BS-statement-2. Three differences, settled from the sources and pinned by `gnucash/tests/gnucash.rs`: GnuCash books an unbalanced entry and parks the difference in `Imbalance-USD` (BS-entry-1 refuses it: Pacioli ch. 36, Pub. 583); it reads a credit of minus 100.00 as a debit (BS-entry-2 is a CONVENTION that removes the ambiguity); it rounds 10.005 to 10.01 silently (BS-ledger-1's CHOICE, found by the first cross-check, is not to). The examples stand in each case. GnuCash has no reversal link, so BS-ledger-5, -6 are not claimed by it.
+   - **Not done, and why.** (a) Done when 3 is met for the rules the schema can show; these stated rules still have no example because the schema has no event or query for them: BS-entry-4 (B-28), BS-ledger-7 (B-20), -9 (B-29), -12 (B-44), BS-asset-2 (B-22), -3 (B-24), BS-revenue-1 (B-17), BS-arap-1 (B-18), BS-arap-6 (B-42, whose allocated names `arap-settlement-exact` and `processor-fee-gross-presentation` wait on a payment/settlement event and an aging query), BS-format-1 (B-27); each section says why. B-39, B-40, B-43, B-45 are unstated in `rules.md`. (b) Step 6, the repository of its own, is the owner's call (a public repository, CC BY 4.0 for the text) and waits on step 5 being stable; nothing was pushed. (c) The derivation covers the ledger-core examples; depreciation, schedules, members, 1099s, formats and the cash-flow sections are skipped by the model and checked by the engines only.
+
 
 ### 8.3 P4b reference design: receivables and payables, first class (D-45)