Hegel

Hegel is a property-based testing engine built on Hypothesis, the most widely used property-based testing library, with libraries for Rust, Go, C++, TypeScript, Java and OCaml. The TypeScript library is @hegeldev/hegel. It is in beta.

Like fast-check, it samples inputs and orders; it does not explore every state.

Hegel draws inputs and shrinks failures. Here it finds a quantity bug and an oversell in a stock reservation.

Using Hegel

The code below is in formal-methods-samples/hegel-stock-reservation.

The problem

reserve accepts a quantity of 0 or less, and two reservations started together both pass the stock check.

A shop holds stock for a customer while they check out. reserve checks that there is enough, saves the reservation, then takes the units out of stock:

// inventory.ts (shortened)
async reserve(sku: string, quantity: number): Promise<string | null> {
  if (quantity > (this.stock[sku] ?? 0)) {
    return null;
  }
  const id = await this.deps.saveReservation({ sku, quantity });
  this.stock[sku] = (this.stock[sku] ?? 0) - quantity;
  return id;
}

It has two bugs. The check only compares the quantity with the stock, so a quantity of 0, a negative one or a fraction gets through. And the check runs before the await while the units are taken after it, so two reservations that start together both pass the check against the same stock.

Install and set up

pnpm add -D @hegeldev/hegel

Runs inside your usual test runner (the example uses Vitest); a strict typecheck also needs @types/node.

Writing the check

tc.draw(gs.integers()) asks Hegel for a value; hegel.testAsync runs the test many times.

A Hegel test is a plain async function that gets a test case, tc. tc.draw(generator) asks Hegel for a value; gs.integers() generates any safe integer, and gs.integers({ minValue, maxValue }) limits the range. Any thrown error fails the test case. hegel.testAsync runs the function many times with new draws and rejects if one fails.

The first test draws a stock level and any integer quantity, makes one reservation, and checks that a successful one took units out of stock without going below zero. The save is a stub that resolves at once:

// inventory.hegel.test.ts (shortened)
const deps = { saveReservation: async () => 'r1' };
// No saved failures and no randomness, so every run gives the same result.
const settings = { database: hegel.Database.disabled, derandomize: true };

await hegel.testAsync(async (tc) => {
  const before = tc.draw(gs.integers({ minValue: 0, maxValue: 100 }));
  const quantity = tc.draw(gs.integers());
  const inventory = new Inventory({ mug: before }, deps);
  const id = await inventory.reserve('mug', quantity);
  const after = inventory.stock['mug'] ?? 0;
  if (id !== null && (after < 0 || after >= before)) {
    throw new Error(`reserved ${quantity} of ${before}, stock is now ${after}`);
  }
}, settings);

The second test draws a stock level and two quantities that each fit, and starts both reservations at once with Promise.all. A later draw can depend on an earlier one: maxValue: before keeps each quantity within the stock.

// inventory.hegel.test.ts (shortened)
await hegel.testAsync(async (tc) => {
  const before = tc.draw(gs.integers({ minValue: 1, maxValue: 100 }));
  const first = tc.draw(gs.integers({ minValue: 1, maxValue: before }));
  const second = tc.draw(gs.integers({ minValue: 1, maxValue: before }));
  const inventory = new Inventory({ mug: before }, deps);
  await Promise.all([inventory.reserve('mug', first), inventory.reserve('mug', second)]);
  const after = inventory.stock['mug'] ?? 0;
  if (after < 0) {
    throw new Error(`reserved ${first} and ${second} of ${before}, stock is now ${after}`);
  }
}, settings);

Running it

Both bugs, shrunk: 0 units from an empty shelf, and two reservations of one mug.

The real output of the first test (stack trace left out):

var draw_1 = 0;
var draw_2 = 0;

reserved 0 of 0, stock is now 0

Each draw_N line is one tc.draw call, in order: draw_1 is the stock and draw_2 the quantity. Then comes the message of the error the test threw. Hegel shrinks the failure to the smallest case: an empty shelf and a reservation for 0 units, which succeeds.

The second test:

var draw_1 = 1;
var draw_2 = 1;
var draw_3 = 1;

reserved 1 and 1 of 1, stock is now -1

It finds the oversell too, shrunk to one mug and two reservations of one.

Fixing the bug

Reject quantities below 1 and take the units before the save. Both tests pass 100 cases.

The fix rejects a quantity that is not a whole number of at least 1, and takes the units before the save:

Diff style

async reserve(sku: string, quantity: number): Promise<string | null> {
  if (quantity > (this.stock[sku] ?? 0)) {
    return null;
  }
  const id = await this.deps.saveReservation({ sku, quantity });
  this.stock[sku] = (this.stock[sku] ?? 0) - quantity;
  return id;
}

async reserve(sku: string, quantity: number): Promise<string | null> {
  if (quantity > (this.stock[sku] ?? 0)) {
  if (!Number.isInteger(quantity) || quantity < 1 || quantity > (this.stock[sku] ?? 0)) {
    return null;
  }
  const id = await this.deps.saveReservation({ sku, quantity });
  this.stock[sku] = (this.stock[sku] ?? 0) - quantity;
  const id = await this.deps.saveReservation({ sku, quantity });
  return id;
}

async reserve(sku: string, quantity: number): Promise<string | null> {
  if (quantity > (this.stock[sku] ?? 0)) {
  if (!Number.isInteger(quantity) || quantity < 1 || quantity > (this.stock[sku] ?? 0)) {
    return null;
  }
  const id = await this.deps.saveReservation({ sku, quantity });
  this.stock[sku] = (this.stock[sku] ?? 0) - quantity;
  const id = await this.deps.saveReservation({ sku, quantity });
  return id;
}

async reserve(sku: string, quantity: number): Promise<string | null> {
  if (!Number.isInteger(quantity) || quantity < 1 || quantity > (this.stock[sku] ?? 0)) {
    return null;
  }
  this.stock[sku] = (this.stock[sku] ?? 0) - quantity;
  const id = await this.deps.saveReservation({ sku, quantity });
  return id;
}

With the fix, both tests pass 100 test cases.

Project layout and CI

The Hegel tests are normal test files next to the code. CI runs the tests. Nothing else to install.

./
├── .github/workflows/ci.yml
├── .gitignore                         lists .hegel/
└── src/
    ├── inventory.ts                   the reservation code
    └── inventory.hegel.test.ts        the Hegel tests

Commit the code and the tests. Do not commit .hegel/: Hegel writes the failing cases it finds there on your machine. The native engine comes from npm for Linux, macOS (arm64) and Windows, so CI needs no extra setup. A failing test makes the test run exit non-zero:

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

# .github/workflows/ci.yml (steps)
- run: npm ci
- run: npm test    # vitest run

When the CI or GITHUB_ACTIONS variable is set, Hegel does not save failures and does not draw at random, so each CI run tries the same cases.

What fails when:

A change lets a bad input through: the test, with the smallest draws that break it.
A change adds a race between async calls: only if the one order Hegel runs shows it. It does not try other orders.

Making changes

Change the code, draw any new input, run the tests, commit.

Change the code.
If it takes a new input, draw it with tc.draw in the test.
Run npm test. A failure prints the draws (draw_1, draw_2, …) and the error.
Fix the code and run the tests again.
Commit the code and the tests together.

Strengths

It runs your real code. You write normal tests that ask for generated values.
It is strong on data. It found the quantity-0 bug from generated inputs, and cuts a failure down to the smallest input that still fails.
A failure comes back. It saves the smallest failing input and replays it on the next run.
It runs in many places. In TypeScript it works on Node, Bun and Deno, and in the browser.

Limitations

A clean run is not a proof. It tries a sample of random inputs (100 cases in the example), not every input.
It does not control the order of async calls in TypeScript yet. Every case ran one order of events, so other orders of the reservations and their saves were never tried. fast-check can try random orders of promises, and pnueli, TLA+ or Quint check every order in a model.
The TypeScript library is in beta. The example uses version 0.4.6.