A checker, measured

Where does a business break when two things happen at once?

A business is a set of processes that run at the same time. Guests order while the kitchen cooks. A booking form shows free slots while the desk fills them. Each process is simple, and each is right on its own. The trouble starts where they meet.

A model checker finds that trouble before a customer does. It takes a small model of the business and tries every order in which its steps can happen. Wherever a rule breaks, it gives the shortest path there. TLA+ is the language such models are written in, and TLC is the checker that runs them. We wrote six small businesses this way and checked each one.

Try it yourself

Where does your business break?

Six example businesses, each with a rule that breaks and the fix that mends it
Your own business, described in a few sentences and written as a model for you
100,000 episodes of what it earns, as written and with your fixes on

Checking is free. Playing episodes needs a sign-in, and writing your own business is billed like any workbook run.

Check a business

Continue in

One business, step by step

Two tables and one fish

The restaurant has five processes: the guests, the kitchen, the stock, the supplier and the till. There are two tables and one fish on the board. The checker reaches 184 states, and one of its three rules breaks: never sell a fish that is gone. This is the shortest path to the break.

1Table 1 sits down.1 fish on the board
2Table 2 sits down.1 fish on the board
3The server reads the board for table 1.table 1 has seen 1 fish
4The server reads the board for table 2.table 2 has seen 1 fish
5Table 1 orders the fish.1 ticket waits
6Table 2 orders the fish.2 tickets wait for 1 fish
7The kitchen cooks table 1's fish.0 fish left
8The kitchen tells table 2 the fish is gone.the rule breaks

No step here is wrong. The server read the board for each table while the fish was still there. Both tables ordered, and only one could be served. The bug lies in the gap between reading the board and cooking the fish. A plan that is read one process at a time never shows that gap.

Fixes, each tried on its own

Why the obvious fix is not enough

Each fix changes when a step can happen. The checker tries each one alone and says whether its rule then holds in every state it can reach.

Fix, turned on alone	Rule it is for	States reached	The rule
Read the board again when the order is taken	never sell a fish that is gone	184 of 184	still breaks
Take the fish off the board when it is ordered	never sell a fish that is gone	180 of 184	holds
Close the kitchen when no ticket is waiting	the kitchen closes only when no ticket waits	184 of 184	still breaks
Last orders: close when no table is seated, choosing or waiting	the kitchen closes only when no ticket waits	121 of 184	holds

Reading the board again is the fix most owners would try first. It does not help. Both tables can order while the one fish is still on the board, so the second check passes too. Taking the fish off the board the moment it is ordered closes the gap. The second table then sees nothing left to order.

The kitchen’s rule works the same way. Closing when no ticket waits still breaks, because a table that is still choosing can order after the kitchen has closed. Last orders holds. With both working fixes on, the checker reaches 107 states and every rule holds.

Six businesses

The same shape, six times

Each example has one rule that breaks only because two processes interleave. In each, the obvious fix still breaks and a second fix holds. Each step that earns or costs money carries a reward, so the page can play 100,000 episodes and show what the bug costs.

Business	The rule that breaks	Steps to the break	Still breaks	Holds	Reward an episode, as written and fixed
Restaurant184 states	never sell a fish that is gone	8	read the board again	take the fish off the board	22.99 → 37.83
Food truck143 states	never take money for tacos the grill cannot make	6	wipe the board at once	each order holds a tray	6.31 → 10.51
Coffee shop98 states	never sell a latte there is no milk for	3	update the app at once	an app order holds its milk	-0.81 → 6.00
Vending machine206 states	every card charged for a jam gets its money back	4	no sale while the timer runs	write each jam on a list	-2.61 → 2.99
Cleaning business386 states	the cleaner is never booked twice at the same time	6	check again on send	send holds the slot	86.77 → 97.61
Battery cell factory392 states	a batch that failed its test never ships	4	check again at the dock	every batch starts on hold	39.96 → 40.13

Episodes that reach a broken state, out of 100,000 for each business

Restaurant39,000 as written, 0 fixed
Food truck42,500 as written, 0 fixed
Coffee shop45,400 as written, 0 fixed
Vending machine37,400 as written, 0 fixed
Cleaning business13,800 as written, 0 fixed
Battery cell factory34,100 as written, 0 fixed

In all six businesses, the fixed version earns more in an average episode. The amounts differ a great deal. The coffee shop and the vending machine lose money as written and make money when fixed. The battery factory earns almost the same either way, 39.96 against 40.13. Its fix keeps a failed batch from shipping, and that rule matters even where the money hardly moves.

On the try page

Model your own business

Pick Your own on the business plan checker and describe the business in two or three sentences. A bakery, a bike rental, a dental clinic and an ice cream stand are there to start from. A model writes the description as a spec of processes, steps, rules and fixes. The page then checks it at once, up to 5,000 states, and keeps it in your account beside the examples.

A few things make a model worth checking.

Keep it small. Two or three tables, customers or batches are enough to show an interleaving.
Make each process simple and plainly right on its own.
Write one rule that can break only when two processes interleave, such as a check and an action that are not one step.
Write one rule that holds, so the checker proves something as well as finding something.
Put a reward on each step that earns or costs money, between 1 and 100.
Name each fix's rule and the link where it acts. The map then marks that link when the fix is on.

Continue in, beside the map, hands the business to ChatGPT, Claude or another assistant. It copies the rules that break, the fixes you turned on and the rewards. It also copies the whole business as a TLA+ module, which the assistant can change and check with TLC.

From your agent

A TLA+ workbook that TLC checks after every edit

An agent connected to hedwigai over MCP can keep a business model as a workbook. Put the module in a tla fence, with its config in a cfg fence or in the trailing \* Name.cfg: comments that the page’s export writes. A .tla file on a connected drive can start a workbook too.

Every edit a run makes to that module goes to TLC before it is kept. A module that does not parse, or that TLC cannot run, is handed back to the model with TLC’s own error, and the edit is tried again. A rule that breaks is not an error. TLC reports it with its shortest trace, and the version is kept, because finding broken rules is the point of the model.

This is the restaurant, asked for one edit:

create_workbook  name: "Restaurant"
                 document: "# Restaurant\n\n```tla\n---- MODULE Restaurant ----\n…"

update_workbook  instruction: "In the TLA+ module, make OrdersTheFish
                 also require fish > 0, so the server reads the
                 board again when taking the order."

get_trace        PATCHED: TLC: 121 states; NoFishSoldThatIsGone
                 breaks after 8 steps (24 reachable states break
                 it) (5.2 s)

That run already had last orders on. The model made the edit in 11 seconds, TLC checked it in 5.2, and the whole run took 107 seconds. TLC found what the page finds. Reading the board again leaves the fish rule broken, after the same 8 steps.

Add hedwigai to your MCP client from mcp.hedwigai.com, or sign in with a work email. Then ask your agent to model your business as a TLA+ workbook and check it with TLC.

Try it yourself

Where does your business break?

Six example businesses, each with a rule that breaks and the fix that mends it
Your own business, described in a few sentences and written as a model for you
100,000 episodes of what it earns, as written and with your fixes on

Checking is free. Playing episodes needs a sign-in, and writing your own business is billed like any workbook run.

Check a business

Continue in

More head-to-head evals

GLM-5.3 against DeepSeek V4.1 Flash on 75 questionsTwo models answer the same 75 questions; one is always right, the other 14× cheaper.

Measure	GLM-5.3	DeepSeek V4.1 Flash
Right, of 75	75	71
Seconds a question, median	3.9	1.8

Read the comparison How we made a long-running AI agent for knowledge work 4× fasterOne cited knowledge work task through 13 experiments: 937 s to 233 s, with the model held constant.

Measure	First run	Best since
Landscape, seconds	937	233
Memo, seconds	759	602

Read the report Ten models plan a change to a spreadsheet: which do it in under a minute, traced call by callTen models drive one agent harness through the same spreadsheet request; six write the plan, timed and traced call by call.

Measure	Qwen3 235B	GLM-5.2	Gemini 3.8 Flash	Claude Opus 5
Seconds to the plan, median	27	48	57	94
Plans written, of three runs	2	3	3	3

Read the comparison SubQ, jev, Perplexity's Decider and Bespoke's Nimble on biotech diligence memos: finding the sentences a column is aboutFour decision models judge every sentence of ten biotech diligence memos for five columns, scored against sentences a person marked.

Measure	SubQ	jev	Decider	Nimble
Found, mean of five columns at section length	64%	65%	66%	68%
Mechanism of action, found at section length	57%	51%	61%	54%

Read the comparison Leads with a reason to write: hedwigai ask, Apollo and treg on one brief40 leads each, every one checked: the right person, an inbox that accepts, and a dated reason to write.

Measure	ask	Apollo	treg
Usable leads	13 of 40	7 of 40	6 of 28
Cost per usable lead	$0.037	$0.27	$0.23

Read the comparison Self-hosted decisions for ask: Perplexity's open Decider in place of jev on 92 company questionsThe decisions inside hedwigai ask made by Perplexity's open Decider on two NVIDIA RTX 3090s, against jev.

Measure	ask with jev	ask with Decider
Questions right, of 92	89	89
Wrong answers	1	2

Read the comparison Clinical decisions: jev and ask on System One, PubMedQA, SciFact and a 370-decision setEdgeEvals' System One board, PubMedQA, SciFact, and a clinical set built to System One's rules.

Measure	jev	ask
Our 370 clinical decisions, right	94.6%	93.0%
PubMedQA, right (best EdgeEvals scored: 62.2%)	77.0%	74.4%

Read the comparison Executive lookup for US-listed companies: Claude Opus 5.5 and ask on 95 questionsWho runs a public company, and how to email them: a frontier model from memory against hedwigai ask.

Measure	ask	Claude Opus 5.5
Questions right, of 95	59	63
Small companies right, of 20	13	9

Read the comparison Rental comps: floor-plan rents and amenities on 14 listings, five assistants comparedRent per floor plan and amenities for US rentals: hedwigai realestate-us against Claude, GPT, Gemini and Perplexity with web search.

Measure	realestate-us	Best of four assistants
Floor-plan rents right, of 26	26	23
Amenities claimed the listing doesn't state	12	129

Read the comparison Company screening from SEC filings: jev, Vela 2.0 and ask on 92 yes/no questionsYes-or-no questions about public companies, answered by two decision models alone and by hedwigai ask.

Measure	ask	jev
Right, of the questions answered	98%	79%
Wrong answers, of 92	2	19

Read the comparison Defect localization in industrial images: four frontier models and a trained localizerFour frontier models asked to put a box around what they just described.

Measure	Trained localiser	Best of four frontier models
Mean overlap with the defect (IoU, 0 to 1)	0.421	0.109

Read the comparison