"Model" now mostly means a large language model. The models this blog is about are the other kind — a Petri net with a few dozen places that we can execute directly, read on one screen and check properties of — and the claim here is that they matter more with LLMs around, not less, because an LLM is most useful when one of them is constraining it.
A model is an abstract representation of a process: behaviors (actions) plus attributes (data). A good model makes a system predictable and easier to understand. A great model reduces code complexity.
LLMs are impressive at generating text and code, but we can't inspect their reasoning, prove properties of their behavior or compose them predictably. Small formal models like Petri nets make the opposite trade:
| Property | LLMs | Petri Nets |
|---|---|---|
| Inspectable | No | Yes |
| Composable | Awkward | Native |
| Provable properties | No | Yes |
| Executable | Via code gen | Directly |
| Human-readable | Sometimes | At this size, yes |
| Size | Billions of parameters | Dozens of nodes |
Petri nets sit at a rare intersection: visual enough for people to reason about, mathematical enough for analysis, directly executable, and compositional. The coffee shop model is a good size to look at. Here is one drink, copied from NewInventoryNet in go-pflow's examples/coffeeshop/inventory.go:
// Espresso: 18g beans, 30ml water, 1 cup
net.AddTransition("make_espresso", "consume", 200, 150, nil)
net.AddArc("coffee_beans", "make_espresso", 18, false)
net.AddArc("water", "make_espresso", 30, false)
net.AddArc("cups", "make_espresso", 1, false)
net.AddArc("make_espresso", "beans_used", 18, false)
net.AddArc("make_espresso", "water_used", 30, false)
net.AddArc("make_espresso", "cups_used", 1, false)
The whole net is that pattern repeated — six drinks, a sugar transition and six refills, so 13 transitions over 18 places (stock, used and supply for each of six ingredients) — in one function. From that topology we get an ODE simulation for capacity planning: run with the file's own rates it says milk runs out first, not cups, and the coffee shop post has the numbers and the correction. We also get conservation laws we can read straight off the paired arcs — every arc that takes w out of coffee_beans puts w into beans_used, and every refill moves tokens from beans_supply into coffee_beans, so stock + used + supply is constant for each ingredient. That was checked by reading the arcs; the example has no test that asserts it. Deadlock detection is the weakest of the three here. AnalyzeInventoryReachability runs on this net, but the _used accumulators make it unbounded, the search is capped at 1,000 states, and TestInventoryReachability only checks that the analysis completes.
The interactive coffee shop app is served by petri-pilot, and petri-pilot's own generated coffeeshop example is a smaller, separate net — 8 places and 12 transitions, order → make → serve, with espresso drawing 20g of beans rather than 18. The two haven't been reconciled.
When we treat the model as the artifact rather than the code, the order of work changes: we sketch the topology, validate behavior with simulation, and extend monotonically. Code becomes a derived output.
Unlike LLM output, a Petri net comes with questions we can actually put to it. Reachability asks whether, from a given state, the system can get to a target state — is this workflow completable? Boundedness asks whether it stays within limits, whether a queue can overflow. Liveness asks whether the net can deadlock and under what conditions it halts. These are the failures that take production systems down, and on a net we can ask about them before writing implementation code — with the caveat the coffee shop already showed, that a net with accumulators or large markings runs exhaustive search out of room, and the question has to be asked of a bounded version.
The ODE finds structure that isn't obvious by eye. In the tic-tac-toe model the empty-board scores come out 1.27, 0.95 and 0.63 for center, corner and edge — the ratio 4 : 3 : 2, which is the number of win lines through each cell. No game heuristic is encoded; the ranking falls out of the topology. It is a strategic prior, though, not a strategy. Tested against exact minimax in August 2026, the plain ODE missed the fork and lost 7% of games as O, and it took declaring the opponent's policy as extra structure to make the evaluator minimax-equivalent (the correction and its resolution). The missing piece turned out to be more declared model, not search.
What we've learned building the pflow ecosystem is that LLMs are most useful when formal structure constrains them — LLMs for models rather than LLMs or models.
What-if analysis starts from a plain-English description of a business — a vet clinic, a coffee shop — and has the LLM draft the net; the simulation then does the part the LLM can't be trusted with, which is saying what a change in staffing or demand actually does. That line of work has since become sim.pflow.xyz, where a model can be calibrated against your own data. Code-to-flow runs the other way into a model: paste code in any language, Claude proposes places and transitions, and petri-pilot's validator checks the structure before the model is returned (pkg/serve/codetoflow.go). The LLM does the messy pattern recognition and the validator decides whether the output is a well-formed net — though well-formed is not the same as faithful to the code, and we haven't found a check for the second in that path.
Petri-Pilot goes from a model to a full application — frontend, backend, event-sourced state. An earlier version of this post said Claude writes that code. It doesn't: generation is deterministic, templates compile the model and the same model always produces the same code, while the LLM's job is designing the model (petri-pilot also runs as an MCP server for that). What the model constrains shows up in the generated tests: the coffeeshop example's TestCannotFireDisabledTransition fires a transition the current marking doesn't enable and expects the app to refuse it (workflow_test.go). The book — twenty chapters and an epilogue — was written with LLM help, with the examples built on executable nets.
The model is the checkpoint between human intent and machine execution, and it works as one because it is small enough for a person to read.
The ecosystem now supports both directions:
Model-first (design new systems):
pflow.xyz (edit model) --> ODE simulation (validate) --> petri-pilot (generate app)
Code-first (understand existing systems):
existing code --> code-to-flow (extract model) --> pflow.xyz (inspect/edit) --> generate new code
Both pipelines keep the model as the source of truth. The model is where humans verify correctness; code flows from it and back to it.
Small models won't write your marketing copy, and LLMs won't prove your system is deadlock-free; the interesting question was always how they fit together. The arrangement we keep landing on puts the LLM at the edges — turning a description or a codebase into a candidate net — and keeps it out of the middle, where the net's firing rule, the validator and the ODE decide what's true. That is a design choice, not a measured result. This post has no number for how often an LLM-drafted net is wrong in ways the validator can't see, and that is the number that would say how much of the middle an LLM could eventually be trusted with.
For readers of the March version (revised 2026-09-26):
cell/func/arrow syntax that exists nowhere in the pflow repos, with names (brew_espresso, beans) that don't match the model. It is replaced with the actual Go from go-pflow, and the conservation and deadlock claims are now stated at the strength the example earns.Related: The Model Is the App · Coffee Shop Model · Tic-Tac-Toe Model · Code-to-Flow · Introducing Petri-Pilot