spectastic Examples
Worked example · multi-spec · Java

Five specs, one ledger, proven to the cent

A real-time position, portfolio-weight, and FIFO/LIFO/HIFO tax-lot engine — the kind of thing a trading desk runs — built in Java 21 + Quarkus. It's too big for one spec, so spectastic decomposes it: an umbrella and four child slices, driven all the way from principles to a verified terminal state. The proof isn't a toy you poke — it's a passing test suite you can re-run.

Multi-spec Java + Quarkus Enterprise Verified
▷  Try the calculator Read the build →
The product

One append-only trade ledger is the single source of truth; every analytic — net position, portfolio weight, tax lots — is a deterministic pure fold over it, in exact integer money. That one architectural choice is why the live fast-path and a from-zero replay are the same function, and reconcile to the cent. Where the other examples run in your browser, this one is a real backend: the proof is mvn verify22 tests, green.

Five specs, one ledger

The other examples are single specs. This one is the first that shows spectastic slicing a problem too big to hold in one artifact — an umbrella that owns the shared model and the reliability envelope, and four children that each own one hard thing. The links are reciprocal and validated: a child names its <spec-parent>, and the umbrella carves it out with a matching defer-to — or validate fails.

001 · portfolio-analytics umbrella — shared model + reliability envelope 002 · trade-ledger append-only · replay 003 · position-engine net qty · VWAP · MTM 004 · portfolio-weights gross/net · concentration 005 · tax-lots FIFO/LIFO/HIFO the append-only trade ledger — one source of truth every slice folds 20 lifecycle artifacts + an applied change · all validate at the enterprise gate

The lifecycle, to verified

Same eight-verb lifecycle as the rate-limiter build — but this one runs it to the terminal state: every slice ends accepted with a verify.html that ties each success criterion to the test that closes it.

1

Principles → spec

init --profile enterprise seeds 20 principles; then the problem is sliced. The umbrella owns the shared TradeEvent model and a latency ladder that rungs up to tick-to-analytic p99 < 1 ms; each child owns one hard problem. Every NFR across the five specs carries a <spec-slo> — the enterprise gate refuses a "fast".

2

Design → tasks

The umbrella design carries the load-bearing, grounded decisions the whole build inherits: event-sourced folds (D-001), exact integer money at scale 1e-4 (D-002), and the Java 21 + Quarkus stack (D-003) — chosen against a scored matrix, grounded in a real toolchain probe. Then tests-first tasks per slice.

3

Implement

~1,300 lines of framework-free Java for the domain, with Quarkus touching only the REST edge and the wiring bean (library-first, P-12). The read surface ships dark behind a config flag (P-8); Micrometer times every fold — the SLO instrument, made real (P-15). Read the code below.

4

Verify — the terminal step

Each slice moves to accepted and grows a verify.html — a derived view tracing every success criterion to its closing test and every NFR to its SLO. Authoring it wasn't ceremony: the cross-file rules caught a real traceability bug (a task over-citing a criterion it didn't close) that a hand-wave would have shipped. "Done means verified" (P-7), enforced. See it below.

Understand it with the coach

Five specs and a Java service is a lot to land on a new teammate. This is exactly what the extended verb spectastic.explain is for — a grounded coach that explains a real spec, requirement, or decision on demand, from the source. It writes nothing, and it refuses to invent: ask for something that isn't there and it reports the miss instead of hallucinating an answer.

$ spectastic.explain 005-tax-lots FR-002 --proficiency=wheels
 
FR-002 — a sell MUST relieve open lots by the configured policy:
FIFO (oldest), LIFO (newest), or HIFO (highest basis), split the boundary
lot on a partial sell, and realize gain = proceeds − relieved basis.
 
grounded in  specs/005-tax-lots/spec.html#FR-002 · design D-004
history     HIFO landed via change 2026-07-22-hifo-relief (applied)
try it       the calculator below is this rule — flip FIFO / LIFO / HIFO
# it won't invent what isn't there
$ spectastic.explain 005-tax-lots FR-099
no requirement FR-099 in 005-tax-lots.
  the coach reports the miss — it does
  not fabricate a reference. (FR-001…005)
# onboard onto the whole umbrella
$ spectastic.explain 001-portfolio-\
   analytics --course
wrote .spectastic/courses/… (git-ignored)
  a grounded walkthrough of all five slices.

explain is read-only and ephemeral — it teaches an artifact that already exists, authors nothing, and (with --course) can leave behind a git-ignored study guide. More in the extended commands.

Play · read · trust

The payoff, three ways. Play the tax-lot rule in your browser; read the Java that implements it; trust the passing suite that proves it.

PlayFIFO vs LIFO vs HIFO — realize a gain

You hold three lots — 100 @ $10, then 100 @ $14, then 100 @ $12 (deliberately out of order, so all three policies differ). Sell some shares and choose which lots to relieve. Same trades, different policy, different realized gain — that's the whole point of tax-lot tracking, and why HIFO harvests the most.

Lot relief
Realized gain $700.00

A browser re-creation of the Java fold, for illustration. The real thing is TaxLotBook — proven by the tests below, not by this widget.

ReadThree excerpts, each pinned to the decision it implements
Exact money — no double on the money path
public final class Money { // 1 currency unit == 10_000 scaled units (four decimal places) public static final long SCALE = 10_000L; // scale a decimal exactly, rejecting anything finer than 1e-4 public static long of(BigDecimal amount) { return amount.multiply(BigDecimal.valueOf(SCALE)).longValueExact(); } }
→ integer folds are bit-identical on the fast path and on replay. design 001 · D-002
The sign-flip fold — where average cost gets subtle
long newNet = net + fill; if (net == 0 || sameSign(net, fill)) { basis += fill * price; // adding to exposure } else if (Math.abs(fill) <= Math.abs(net)) { basis -= basis * Math.abs(fill) / Math.abs(net); // reduce, keep avg cost } else { basis = newNet * price; // cross zero → reset to crossing fill }
→ a position flipping long↔short doesn't bleed its old basis into the new side. spec 003 · FR-002
FIFO/LIFO/HIFO relief — the rule the calculator plays
while (remaining > 0 && !lots.isEmpty()) { Lot lot = selectLot(lots, policy); // the policy picks the lot; the rest is identical long take = Math.min(remaining, lot.qtyOpen); long gain = take * (sellPrice - lot.basisPerUnit); // exact: basis IS the fill price records.add(new RealizedGainRecord(lot.openSeq, take, gain, …)); lot.qtyOpen -= take; remaining -= take; if (lot.qtyOpen == 0) lots.remove(lot); // full lot consumed (interior, for HIFO) } // FIFO the oldest, LIFO the newest, HIFO the highest cost basis — a scan (D-004) Lot selectLot(Deque<Lot> lots, ReliefPolicy policy) { switch (policy) { case FIFO: return lots.peekFirst(); case LIFO: return lots.peekLast(); case HIFO: Lot best = null; for (Lot lot : lots) if (best == null || lot.basisPerUnit > best.basisPerUnit) best = lot; return best; } }
→ FIFO relieves the head, LIFO the tail, HIFO scans for the highest basis; a partial sell splits the boundary lot. spec 005 · FR-002, design D-004
TrustThe animation illustrates. This passes in CI.
$ export JAVA_HOME=…/temurin-21  # any JDK 21
$ mvn verify
  AnalyticsResourceTest  1/1 ✓  (Quarkus 3.37.3 on JVM, up in 3.0s)
  AnalyticsPlatformTest  1/1 ✓
  LedgerTest          3/3 ✓
  PortfolioWeightsTest   4/4 ✓
  PositionEngineTest    5/5 ✓
  ReconcileToReplayTest  3/3 ✓  # incremental == full replay
  TaxLotBookTest       5/5 ✓  # FIFO 700 · LIFO 500 · HIFO 400
  ──────────────────────────────
  Tests run: 22   Failures: 0   Errors: 0   BUILD SUCCESS

And that suite is wired back to the specs. Each verify.html is a derived trace — a few rows:

criterion / NFRproof
005 · SC-001TaxLotBookTest — FIFO·LIFO·HIFO relief, exact (700·500·400)
001 · SC-001ReconcileToReplayTest — incremental == replay
001 · NFR-001SLO latency · p99 < 1 ms · Micrometer timer

The artifacts

Twenty artifacts — the five slices, each a full spec · design · tasks · verify bundle — plus the applied HIFO change and the Java project. Every one is live and clickable below, and every one passes spectastic validate on the enterprise gate.

001-portfolio-analytics
Umbrella — shared model, reliability envelope, the three grounded decisions
002-trade-ledger
Append-only, gap-free seq, replay, snapshot
003-position-engine
Net qty, VWAP basis, sign-flip, mark-to-market
004-portfolio-weights
Gross/net denominator, sum-to-one, concentration
005-tax-lots
FIFO/LIFO/HIFO relief, partial split, realized/unrealized P&L
↳ hifo-relief
The applied change that added HIFO — three deltas, an adversarial risk pass, tasks folded and drained. Read the proposal →
▷ mvn verifyThe Java + Quarkus project — 22 tests, green · view the source on GitHub ↗

These are the real, rendered artifacts — the same files spectastic validate checks; the excerpts above are drawn from them verbatim.

▷  Try the calculator View source on GitHub ↗ ← All examples