Bombadil

Bombadil is property-based testing for web and terminal user interfaces. Its specs are TypeScript modules with temporal properties. It samples runs of a real UI against temporal properties; it does not explore every state of a model.

A temporal property is a rule about a whole run, not one moment: “there is never more than one order” (always, aka invariant), “the spinner goes away in the end” (eventually), “after Pay is clicked, a receipt shows up” (after this, that).

Bombadil clicks through a running web app and checks temporal properties. Here: a checkout that places an order twice.

Using Bombadil

The code below is in formal-methods-samples/bombadil-checkout. We ran it with Bombadil 0.7.7 and Chrome 153 on macOS. The output is from our run.

The problem

The button stays clickable while the order request is still pending.

A checkout page has a “Place order” button. The click handler posts the order, waits for the server, then adds a confirmation line to the page and hides the button:

<!-- index.html (shortened) -->
<button id="place-order">Place order</button>
<ul id="orders"></ul>

// checkout.js (shortened)
button.addEventListener('click', async () => {
  const response = await fetch('/orders', { method: 'POST' });
  const { id } = await response.json();
  // One confirmation per order the server accepted: <li class="order">Order 1 confirmed</li>
  const item = document.createElement('li');
  item.className = 'order';
  item.textContent = `Order ${id} confirmed`;
  orders.append(item);
  button.hidden = true;
});

The button stays clickable while the request is pending, which takes 500 ms in the sample’s server. A second click in that window sends a second POST. Both requests come back, both handlers append a line, and the page shows two <li class="order"> items: “Order 1 confirmed” and “Order 2 confirmed”. Clicking once and waiting, the way a manual test does, never shows it.

Install and set up

npm install --save-dev @antithesishq/bombadil

Needs macOS or Linux with Chrome, and your app running on a URL.

Writing the check

extract reads the page in every state; always states the rule.

A spec is a plain ES module. Every property and every action generator it exports is used, and the export name is the name in error reports:

import { extract, always } from "@antithesishq/bombadil";
// Keep Bombadil's built-in checks and its default clicks.
export * from "@antithesishq/bombadil/browser/defaults";

// Runs in the browser in every state: how many "Order N confirmed" lines the page shows.
const confirmations = extract((state) =>
  state.document.body.querySelectorAll(".order").length,
);

// The rule, checked in every state: never more than one order.
export const at_most_one_order = always(() => confirmations.current <= 1);

No action generator is needed here: the default clicks find the button.

Running it

It found the double order in all five runs, within 0.9 to 8.7 seconds.

bombadil browser test http://localhost:4500 spec.ts --time-limit=30s --exit-on-violation --output-path out \
  --chrome-grant-permissions=geolocation

--chrome-grant-permissions works around a Chrome 153 error with Bombadil’s default permission.

The last lines of the log, and the report:

00:03.259 Clicking <button> (x: 328.5, y: 126.1, content: "Place order")
00:03.292 Clicking <button> (x: 328.5, y: 126.1, content: "Place order")
00:03.330 Clicking <button> (x: 328.5, y: 126.1, content: "Place order")
00:03.363 Clicking <a> (x: 68.7, y: 228.6, content: "Continue shopping")

at_most_one_order was violated:

as of 00:00.000, it should always be the case that () => confirmations.current <= 1, however at 00:03.389, confirmations = 2

Test finished, finding 1 violation!

Inspect the test results using:

  bombadil browser inspect out

Reproduce this test using:

  bombadil browser test http://localhost:4500/ spec.ts --reproduce out

The exit code was 2. Bombadil clicks about every 35 ms, so repeated clicks inside the 500 ms window happen often. In five runs it found the double order in all five, after 0.9, 1.2, 2.3, 3.4 and 8.7 seconds.

Fixing the bug

Disable the button on click. Two 30-second runs were clean.

The fix: the button is disabled as soon as it is clicked:

Diff style

// Places the order and shows each confirmation the server sends back.
const button = document.getElementById('place-order');
const status = document.getElementById('status');
const orders = document.getElementById('orders');
const continueLink = document.getElementById('continue');

button.addEventListener('click', async () => {
  status.textContent = 'Placing your order...';
  const response = await fetch('/orders', { method: 'POST' });
  const { id } = await response.json();
  const item = document.createElement('li');
  item.className = 'order';
  item.textContent = `Order ${id} confirmed`;
  orders.append(item);
  status.textContent = 'Thank you!';
  button.hidden = true;
  continueLink.hidden = false;
});

// Places the order and shows each confirmation the server sends back.
const button = document.getElementById('place-order');
const status = document.getElementById('status');
const orders = document.getElementById('orders');
const continueLink = document.getElementById('continue');

button.addEventListener('click', async () => {
  button.disabled = true;
  status.textContent = 'Placing your order...';
  const response = await fetch('/orders', { method: 'POST' });
  const { id } = await response.json();
  const item = document.createElement('li');
  item.className = 'order';
  item.textContent = `Order ${id} confirmed`;
  orders.append(item);
  status.textContent = 'Thank you!';
  button.hidden = true;
  continueLink.hidden = false;
});

// Places the order and shows each confirmation the server sends back.
const button = document.getElementById('place-order');
const status = document.getElementById('status');
const orders = document.getElementById('orders');
const continueLink = document.getElementById('continue');
button.addEventListener('click', async () => {
  button.disabled = true;
  status.textContent = 'Placing your order...';
  const response = await fetch('/orders', { method: 'POST' });
  const { id } = await response.json();
  const item = document.createElement('li');
  item.className = 'order';
  item.textContent = `Order ${id} confirmed`;
  orders.append(item);
  status.textContent = 'Thank you!';
  button.hidden = true;
  continueLink.hidden = false;
});

// Places the order and shows each confirmation the server sends back.
const button = document.getElementById('place-order');
const status = document.getElementById('status');
const orders = document.getElementById('orders');
const continueLink = document.getElementById('continue');

button.addEventListener('click', async () => {
  button.disabled = true;
  status.textContent = 'Placing your order...';
  const response = await fetch('/orders', { method: 'POST' });
  const { id } = await response.json();
  const item = document.createElement('li');
  item.className = 'order';
  item.textContent = `Order ${id} confirmed`;
  orders.append(item);
  status.textContent = 'Thank you!';
  button.hidden = true;
  continueLink.hidden = false;
});

Against the fixed page, two 30-second runs finished with “Test finished after time limit!” and exit code 0. Both reached a confirmed order, and none showed a second one. That is evidence, not proof: a clean run means nothing was found in this run.

Project layout and CI

Commit the spec next to the app. CI starts the app and runs Bombadil in Chrome. No API key.

./
├── .github/workflows/ci.yml
├── server.ts             starts the app
├── public/index.html     the checkout page
├── checkout.js           the page script
└── spec.ts               your rules

out/ is not committed: it holds the run’s trace and screenshots. CI needs Chrome and the app running on a URL. GitHub’s Ubuntu runners have Chrome, and Bombadil finds it on the PATH. Chrome needs --no-sandbox there. Bombadil’s own action, antithesishq/bombadil-action, can install Chrome and run the test instead.

The CI workflow: .github/workflows/ci.yml (5 lines)

# .github/workflows/ci.yml (steps), on ubuntu-latest
- run: npm ci
- run: node server.ts &
- run: curl --retry 30 --retry-all-errors --retry-delay 1 --silent --fail http://localhost:4500 > /dev/null
- run: npx bombadil browser test http://localhost:4500 spec.ts --time-limit=30s --exit-on-violation --output-path out --no-sandbox --chrome-grant-permissions=geolocation

What fails when:

The run breaks a rule: Bombadil exits with code 2 and prints the clicks that led to it.
The app is not running: Bombadil exits with code 1.
Nothing is found: exit code 0. The run tried only some clicks and timings, so a later run can still find a bug.

Making changes

Change the page, run Bombadil locally for longer, add rules to spec.ts, commit.

Change the page.
Run Bombadil locally against it, with a longer --time-limit than CI.
If the change needs a new rule, export it from spec.ts.
When a rule breaks, look at the run with bombadil browser inspect out.
Commit the page and the spec together.

Bombadil’s manual also suggests running longer tests on a schedule, for example on the main branch.

Strengths

It tests your real app. It clicks through the page in Chrome, and you write no model of the app.
It finds bugs before you write any rule. Its default checks come first; your own rules are TypeScript, such as “never two orders”.
You can watch the bug. It records the clicks that broke the rule, and you can replay them.

Limitations

A clean run is not a proof. It tries a random sample of clicks and timings. For every order, pnueli, TLA+ or Quint check a model instead.
It sees the page, not the logic behind it. Which reply arrives when, or what a retry does, shows only through the timings the run happened to try.
A replay may not show the bug again. The same clicks can get different timings on the next run.
It is still early. It needs Chrome on macOS or Linux, and the API may change between versions.