SPINACH is a VSCode extension with a three-phase pipeline, each phase gated by developer review.

1. Concept model. An LLM agent crawls the running application and decomposes it into concepts in Daniel Jackson's sense (Jackson 2021): units such as User, Article or follow, each with a purpose, an operational principle, state fields, actions and invariants, plus synchronizations that tie concepts together. The agent may infer actions it never reached: a trash concept implies a "remove from trash" action whether or not exploration saw the button.
2. Natural-language properties. A second agent derives properties per concept and synchronization. It is deliberately not told it is writing property-based tests; the authors report that framing biased output toward "very mathematical, but inconsequential" properties.
3. LTL and Bombadil. A final phase formalizes each approved sentence into LTL where it can, then emits a Bombadil test.

The paper's worked example: "a user must be logged in to follow another" becomes \(G(\mathit{following} \rightarrow \mathit{authenticated})\). The generated Bombadil test is an always over two extractors: when the viewer is unauthenticated and on a profile page, the follow button's label must not start with "Unfollow".

Two open-source applications, both previously used to evaluate GUI-testing tools.

Very few specifications were fully formalized in LTL. Most of the remainder were entity-relationship constraints ("every card belongs to exactly one board") that need first-order quantification, which propositional LTL lacks. Accuracy was assessed on a sample of five specifications, judged by the first author and then discussed with the second; the paper reports no score.

The generated tests compiled. They found no bugs in either application. The authors attribute this to Bombadil's execution model rather than to the properties: actions are chosen by weighted random selection, so states behind a login, a navigation and a form fill are rarely reached, and an LLM-generated selector that misses the real DOM never fires at all.

Everything else is planned: mutation testing for RQ1 against two baselines (crawl then PBT directly; crawl then EARS requirements then PBT, the Kiro route), running tests across real version histories as a less synthetic fault source, an ablation that strips concepts down to purpose and operational principle, and a user study for RQ2 on legibility and maintenance. Proposed fixes: replace random action selection with constrained trace generators that synthesize directed interaction sequences (Zhou et al. 2026), and reconsider LTL itself, citing evidence that non-specialists misread it (Greenman et al. 2023).

Bombadil, and Quickstrom before it (O’Connor and Wickström 2022), gives the author LTL over browser state and assumes the author knows which properties matter. SPINACH keeps that checker and replaces the author. The interesting result is what the inferred properties look like once checked.

• They are state invariants. The worked example is a single \(G\) over a propositional implication. Nothing in the paper exercises eventually or within, the operators that make Bombadil more than an assertion library. Conjecture: concept invariants, by construction, compile to safety properties of one state, so the temporal half of the language goes unused.
• The extractor problem moves, it does not go away. The worked test returns true when the follow-button label is null. If the selector is wrong, the property passes on every state. This is the null-returning logo extractor from 4, generated rather than written, and it fails in the quiet direction. The paper names "imperfect selectors" as one cause of zero findings; this note's checklist item 3 (verify each selector against the live DOM) applies unchanged to generated tests.
• Exploration is the bottleneck in both. The navigation stalls and quiescence notes in 3 are the hand-written version of the reachability limit the paper hits. Neither gets better by improving the properties.

Context Surfaces separates context a system emits from context a worker elicits, and files property-based driving under the second. SPINACH's crawl reads the DOM surface, but its properties come from two places, and only one of them is the surface.

The concept model's own integrity notes say a design choice "is the standard design for this class of app." That is the model's prior, not anything the page showed. The trash example is the same move: a state inferred because apps of this kind usually have it. Inferring past the surface is how SPINACH finds properties nobody exercised; it is also how a property comes to assert a "Home" link the site never had, the second false positive recorded above. The paper's developer-review gates are where that gets caught, so the review step is the mechanism that keeps the inference honest, not an add-on.

Some of the properties are not on the surface at all. "Email must be unique across all users" cannot be observed from one browser session; one user's DOM never shows every other user's email. Conjecture: part of the paper's formalization gap is a surface gap. These are database-surface properties reached through a DOM-surface tool, and no choice of logic fixes that.

• Calibration. Zero bugs found on two apps is an uncalibrated result. Until the suite has run against a known-bad build and gone red, a green run says nothing about the apps; the paper's planned mutation and version-history runs are exactly the calibration missing so far. The site's rule (a gate never run against a known-bad input is uncalibrated) applies directly, and the authors make the same point in their own terms.
• Oracles. The crowsnest rig checks the receiver against an independent model that re-derives expected state from the spec after every step. A Jackson concept already has state, actions and invariants, which is most of such a model. Conjecture: an executable concept, stepped alongside the browser, would be a stronger oracle than the per-state LTL sentences, and it would cover the entity-relationship constraints that do not fit propositional LTL.
• Shrinking and pin-on-find. With no violation, there was nothing to shrink or pin. When one fires, the shrink discipline carries over with Bombadil's substitutes: the recorded trace and --reproduce replace the seed, and the minimal trace becomes the pinned regression. Nothing in SPINACH changes that step.
• Where it fits. As a generator of candidate properties for a human to review, SPINACH matches what these notes argue: the 94 and 161 sentences are a reading list for whoever writes the suite, and the share on authentication suggests where the model's attention goes. As an oracle that runs unattended, it does not yet fit: the properties are uncalibrated, the extractors are unverified, and the exploration that would exercise them does not reach the states they constrain.

Daikon infers likely invariants from observed traces (Ernst et al. 2001); SPINACH infers them from a model of what the application should be. Conjecture: the failure modes mirror each other. Trace mining fits too closely to what happened; prior-driven inference fits too closely to what usually happens in apps of this class. The first misses properties the traces never violated, the second asserts properties the site never had. The review gate exists for the second.