pflow-polyglot is a repository with one idea in it: a single coffee-machine Petri net, implemented over and over, with every implementation held to a byte-identical six-line trace. The interesting axis is the forms more than the languages: the same net encoded as runtime data (interpreter), as pure functions (lambda), as generated code, and as a public API surface (contract). Four encodings, one golden trace, and a Bazel gate that fails if any of them drifts.
This week the repo picked up a tenth language and, because of it, a fifth form. The language is Lean 4. The form is called proof, and the reason it exists is the point of this post: the theorem declaration in the Lean version is line-for-line equivalent to a runtime check the other languages were already capable of. Writing them side by side is the clearest illustration I have found of what a proof assistant actually buys you — and what it doesn't.
Lean went in the ordinary way first: interpreter, lambda, and contract forms,
mirroring the Haskell ones. Pure functions, Option Marking doing the work the
imperative languages need a prepare/execute split for. Nothing exotic.
But the language kept editorializing. The interpreter form's scheduler — "fire
the first enabled transition until none is enabled" — had to be declared
partial def, because termination of that loop is a property of this net,
not something the compiler can see from the code. Every other language in the
repo runs the same loop without comment. Lean is the only one that makes you
put in writing that you haven't proven it stops.
That asymmetry nagged. The repo's whole premise is that every implementation
makes the same claims about the same model. Lean was pointing out, correctly,
that most of those claims were assertions — comments, at best. The net is
1-safe: says who? Every form carries an enablement clause that refuses to fire
a transition into a marked place, and the README asserts the clause matches
capacity: 1 in the model. Nobody checks that the clause ever matters.
The fifth form drops the assertion and does the work. Two changes to the setup:
Then, before printing anything, the program explores the entire reachable state space by breadth-first search and verifies two claims:
Claim 1 — 1-safety is structural. No reachable marking holds two tokens
in any place, even without the capacity clause. This is the claim that
licenses every other form's set representation: the clause they all enforce is
never load-bearing, and a Set loses nothing a multiset would keep.
Claim 2 — the outcome is confluent. The net has no conflict — no two
transitions compete for a token — so every maximal firing sequence ends in the
same deadlock, and it is exactly {Payment}. The golden trace's final line is
not one schedule's artifact; it is the only place the net can stop.
The search needs no bound to terminate: a marking that violates claim 1 fails
immediately, so the explored space is a subset of {0,1}^10 — at most 1024
markings. This net reaches 16; the whole space, 16 markings and 26 edges, is
checked in as
parity/reachability.golden.
Only after both checks pass does the interpreter's scheduler run and print the canonical trace. A violation exits nonzero before the first line, which fails the parity gate mechanically: a program that dies cannot print six lines.
Here is the shape of claim 1 in Python — a startup model-check, run on every execution:
def verify():
seen = {INITIAL}
frontier = deque([INITIAL])
while frontier:
marking = frontier.popleft()
if any(count > 1 for count in marking):
return f"1-safety violated: reachable marking {marking}"
...
Go, Rust, JavaScript, and — with some ceremony around associative arrays — Bash all say the same thing. And here is the Lean:
def reachable : List Marking :=
explore 1024 [initialMarking] [initialMarking]
def oneSafe (m : Marking) : Bool :=
m.all (· ≤ 1)
-- ...
theorem reachable_one_safe : reachable.all oneSafe = true := by decide
-- ...
theorem unique_deadlock :
(reachable.filter isDeadlock) = [finalMarking] := by decide
explore is the same BFS the other five languages run — same frontier, same
seen-list, same successor function. decide tells the kernel to evaluate
it: the proposition is decidable, so run the decision procedure and check it
returns true. This is proof by reflection, and the honest way to say it is
that the theorem is the Python function. Same algorithm, same 16 markings,
same comparison at the end. Nothing about the Lean version is smarter.
One difference is forced on Lean. A function the kernel evaluates has to
terminate structurally, so explore carries fuel — 1024, the {0,1}^10
ceiling from above — and a separate theorem, reachable_closed, checks that
every successor of every reached marking was itself reached. That is what
lets the other theorems quantify over the whole state space rather than a
fuel-truncated prefix of it. The Python loop just runs out of frontier.
The difference that matters is when it runs and what failure means:
| check runs | failure means | |
|---|---|---|
| Go, Rust, Python, JS, Bash | at startup, every run | exit 1, no trace |
| Lean | once, during elaboration | the program does not compile |
In Lean, main cannot exist unless the net is safe. There is no code path in
the shipped artifact where the check failed, because the artifact is only
produced after the kernel has watched the entire state space get explored.
The runtime versions re-establish the same fact a few microseconds before
every run; the Lean version established it once, and the binary is the
receipt.
A check you have never seen fail is an assertion with better marketing, so:
mutate the net. Make PourCoffee produce a token into Payment — the place
it reads as a guard — and the net can mint payments. Two tokens in one place,
1-safety gone.
Python, at startup:
proof failed: 1-safety violated: reachable marking (0, 0, 0, 0, 0, 0, 0, 0, 2, 0)
exit 1
Lean, at compile time:
error: Tactic `decide` proved that the proposition
reachable.all oneSafe = true
is false
Same defect, same detection, same BFS finding the same marking. One reports it
as a process exit; the other reports it as the nonexistence of the program.
I find the second error message genuinely delightful: it is not "assertion
failed," it is "I proved your claim is false" — the kernel ran the search,
found the counterexample, and refused to let main be defined on the other
side of it.
Neither failure is one of the repo's gates: the mutation is not checked in as
a test, so the parity gates only ever see the safe net. Reproducing it means
editing the PourCoffee entry in python/proof.py and running
make run-python; on the Lean side the file is now generated, so the extra
arc goes into model.json, then make generate and make run-lean. We have
not re-run either for this revision.
The pitch for proof assistants usually leads with what is unreachable for
ordinary languages: dependent types, mathlib, verified compilers. All real.
But the on-ramp is much shorter than that, and this repo now demonstrates it
in the most literal way I could construct. The property is a decidable
statement about a finite state space in both places. The algorithm is
breadth-first search, written as plain functional code in both places. And the
code is nearly the same modulo syntax — explore in Lean is verify() in
Python with the in-place updates swapped for recursion.
The entire delta between "runtime model-check" and "machine-checked theorem"
here is the word theorem and the tactic by decide. That's it. The proof
form in Go and the proof form in Lean are the same program; Lean just runs the
interesting half of it inside the compiler and makes the result a
precondition of the program existing.
There is a real boundary: decide works because the
state space is finite and tiny. The moment the claim quantifies over an
infinite domain — every net of a given shape, every initial marking, every
fuel value — evaluation stops being a proof strategy and you need induction,
invariants, actual mathematics. The theorems in
lean/proof.lean
(seven of them now; see What Changed) sit deliberately on the near side of that boundary, where a theorem is just
another port of a program you already had. The far side is where it stops
being a polyglot exercise — one net, proven safe for all markings, is a
different post.
The repo now stands at 39 programs: five forms across ten languages, gaps deliberate (Solidity cannot model-check itself at startup; Ruby, Julia and Haskell proof forms are open invitations). Twenty programs run under the hermetic Bazel gate, the rest under the native-toolchain gate, and every one of them — interpreter, lambda, generated, contract, proof — prints the same six lines:
Step #1: BoilWater => BoiledWater,CoffeeBeans,Cup,Filter,Pending
Step #2: GrindBeans => BoiledWater,Cup,Filter,GroundCoffee,Pending
Step #3: BrewCoffee => CoffeeInPot,Cup,Pending
Step #4: Send => CoffeeInPot,Cup,Sent
Step #5: Credit => CoffeeInPot,Cup,Payment
Step #6: PourCoffee => Payment
Thirty-three of them assert that trace is right. Five more re-derive the justification at every startup. One of them proves you couldn't have gotten a different one — and won't compile for a net where you could.
October 2026: the August version said lean/proof.lean held three theorems.
It now holds seven, and it is no longer hand-written: tools/codegen -lang lean
emits it from model.json and derives the theorems from the model
(FORMS.md).
The three original statements — reachable_closed, reachable_one_safe,
unique_deadlock — are regenerated unchanged. The four new ones are
P-invariants, one per basis vector of the left nullspace of the incidence
matrix; codegen finds the basis, and Lean does not trust it, re-checking each
invariant by decide on every reachable marking. We read the generated file
and the spec for this revision and did not re-run the proofs. The Lean excerpt
above is copied from that file, with the lines between its definitions
elided.
Related: Byte-Exact Across Four Languages · A Tiling for Computation · Revisiting the Flows