Refinement Loop Across Heterogeneous Systems: Liquidus Overlay Experience Report

In one sitting a contract-only specification became a shipped, public artifact (aygp-dr/liquidus-overlay, one of the build repos grown from the spec-first grind described in the PRD grind note): an injectable command overlay for the Solidus admin, its command surface derived mechanically from a pinned OpenAPI contract, its state machine checked in TLA+, its history mined from git, hosted on Cloudflare, exercised against three different backends. The artifact is incidental. What is worth preserving is the method – a Lakatosian proofs-and-refutations loop run across a dozen unlike systems, steered by a human who supplied the terministic screen and let the machine hold the context.

This is that method, stated so it can be reproduced. Every claim below names its refutation condition; a method that cannot fail is not a method, it is a mood.

Eleven systems, no two speaking the same protocol, each a potential contract violation surface:

The interesting property is not that these connect. It is that the boundary between any two of them is where the work actually happened – and every boundary lied at least once.

Lakatos's thesis is that mathematics advances not by deduction from axioms but by conjecture, attempted proof, refutation by counterexample, and refinement of the conjecture to survive it. The same shape held here, except the counterexamples arrived as HTTP status codes and native-extension load errors. A catalogue of the refutations, because the refutations are the content:

• Conjecture: the pinned contract exposes 103 paths under /api/v2/platform and /api/v2/storefront. Refutation: the git history of the OpenAPI file shows 25 flat, unversioned /api paths and no v2 anywhere – the split is Spree's lineage, not Solidus's. Refinement: correct the contract's own provenance prose; the bare paths were right all along.
• Conjecture: the overlay cannot be exercised without a live store (the spec said so, and made it a non-goal). Refutation: it ran against a stateless mock and against fixtures the same afternoon. Refinement: the non-goal's stated mechanical reason falls; a narrower boundary survives – see the next entry.
• Conjecture: "jump to record R" is testable against the mock. Refutation: Prism is stateless; TLC returns a six-state counterexample where the mock renders a different record than the one searched. Refinement: jump-correctness is a theorem against a live contract and a refuted invariant against a stateless one. The product's supported boundary, discharged by a checker rather than asserted in a README.
• Conjecture: gem install rails -v '~> 7.2' bundler. Refutation: the package manager rejects a version constraint against two packages. Refinement: split the invocation. (Not every aporia is profound. Some are just a CLI.)
• Conjecture: a real backend bound to 0.0.0.0 is reachable on the LAN. Refutation: the TCP handshake completes but the HTTP response never arrives – only for the Ruby process, only on the non-loopback interface. Refinement: a node reverse-proxy to loopback; the boundary was in the host's packet filter, not the bind.
• Conjecture: the session cookie authenticates the admin's own API. Refutation: requires_authentication defaults true, so the contract answers 401 and ignores the cookie. Refinement: supply the running user's api_key; provenance of the call is the user, but the credential is explicit.

Each refinement is cheap only because the context that produced the conjecture survived the refutation. The machine held every prior boundary in memory while the human moved the frontier. That is the whole trick.

The human interjected roughly twenty times, almost always mid-task: change the config vocabulary to SPREE_URL=/=SPREE_TOKEN, cut the self-congratulatory copy, stack the install snippets, stand up a real store, make it public, add topics. None of these were corrections of error. Each was a re-selection of what mattered – Burke's terministic screen, applied live. A screen that foregrounds one contract backgrounds another; the human owns the screen, the machine owns the consequences.

This is the load-bearing asymmetry. The machine is congruent across systems: it will as happily mine a git history as boot Postgres as model-check a temporal formula. It has no preference. Preference is the human's contribution, and the interjection is its interface. Treating the redirections as interruptions is the category error; they are the specification arriving in instalments.

The liquidus grind's own self-audit, docs/reflection-self-audit.md in aygp-dr/liquidus (public), organises the same territory into six moves; that document in turn applies a "Reflection and evaluation" chapter it does not name further. The session is a worked example of each move – and, more usefully, of where each has a refutation condition.

The reproduction question has a sharper form: if the artifact were lost, what would an agent need to regrow it? The answer is small – spec.org and a pinned SHA – and the smallness is the point. The contract is not documentation of the system; it is the seed the system regrows from.

Properties that held across every system and must hold for the method to reproduce:

• Provenance on every result. No datum crossed a boundary bare. Mock responses carried source · spec-SHA · backend; the overlay stamped its panels; the research agent separated git-confirmed from inferred. When you cannot trust a boundary, you can at least label what came through it.
• Falsification before belief. Nothing was "working" until a command produced the evidence. curl before claim, TLC before "verified", gh api before "the spec says". The refutation catalogue above exists because the belief was always provisional.
• One writable repo. Implementation lived only where implementation was permitted; the contract stayed copy-only. The three spec files were relocated to spec-input/ rather than edited, so a build could never silently fork the thing it was grading.
• Long-running work detached, not awaited. The Solidus build, the vips install, the research agent – all backgrounded, watched for a terminal signal, never blocked on. The human kept steering while the slow systems churned.

This method is wrong, and this report should be revised, if:

• A boundary is crossed with no way to instrument it – if provenance cannot be attached, the falsification-first stance degrades to trust, and the loop is running on faith.
• The human's interjections stop re-selecting what matters and start correcting the machine's errors. That inverts the asymmetry: it means the machine is no longer congruent across systems, and the method is subsidising its incompetence with human attention.
• The context does not survive the refutations – if each counterexample forces re-establishing prior boundaries, the cheap-refinement property is gone and the loop is just expensive trial and error with extra steps.

Not a checklist to be filled but a set of preconditions to arrange:

1. Pin the contract, separate it from the implementation. A source of truth that cannot be edited by the thing consuming it. Copy it in; feed changes back through a graded report, never a silent edit.
2. Give the machine one context and many tools. One conversation holding every boundary; ambient access to shell, git, browser, a model checker, cloud CLIs, and subagents for the archaeology you do not want in the main context.
3. Make every claim produce evidence. Wire the loop so "it works" is unspeakable without a command that shows it. Prefer a counterexample-producing checker to a test suite that only confirms.
4. Background the slow systems; watch for a terminal signal. Never await a build in the foreground. Poll for Listening on or FAILED, keep the frontier moving.
5. Let the human supply the screen, in instalments. Do not demand a complete specification up front. The interjections are the spec; the method's job is to keep the context coherent enough that each one is a cheap refinement, not a restart.

The artifact will differ every time. The method is the invariant.

Written from a single session, 2026-07-01, that produced aygp-dr/liquidus-overlay (public) – and written as a reference for related future work, the method rather than the artifact, so an agent handed only spec.org and a SHA can regrow the rest. Refutation catalogue is drawn from that session's command output – HTTP codes, TLC counterexamples, git diffs – not reconstructed from memory. Contract- history claims are git-confirmed against solidusio/solidus; see the build repo's docs/solidus-api-schema-drift.org. The spec-side history of the same grind is in the PRD grind note.