One Petri net, implemented thirty-nine times: five forms across ten languages, every one of them emitting the byte-identical canonical trace.

Click the image to open the model in the pflow.xyz editor (the model itself travels in the link — nothing server-side to rot). The image is model.svg, committed and rendered from model.json by pflow-xyz's SVG generator; model.json is also what tools/codegen reads.

• Places hold tokens: Water, BoiledWater, GroundCoffee, CoffeeInPot, …
• Transitions move them: BoilWater, GrindBeans, BrewCoffee, PourCoffee, Send, Credit
• Arcs wire places to transitions and back
• One guard: PourCoffee requires Payment to be present, and does not consume it — you cannot pour before paying

The net is 1-safe: a place holds zero or one token, and a transition that would produce into an already-marked place is not enabled.

Every implementation prints exactly this, and nothing else:

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

That text is parity/trace.golden — the contract every implementation is held to. The transition name, then the marking as place names sorted lexicographically. Sorting is not cosmetic: it is the only reason a Go map, a Rust HashSet, a Python set and a JS Set can be compared at all.

The implementations are independent rewrites, so an identical trace is a real claim about the model rather than a shared-code tautology.

It is one trace of twenty. This net has real concurrency — at the opening marking, BoilWater, GrindBeans and Send are all enabled, and 9 of its 16 reachable markings offer a choice. Thirty-nine programs agree on these six lines because they all implement one declared rule: fire the enabled transition whose name is lexicographically least. That rule is normative and lives in FORMS.md; the golden is what enforces it.

What the rule does not decide is the outcome. All 20 maximal firing sequences end in {Payment} — the net is confluent, which the proof form checks exhaustively. The scheduling policy chooses which trace gets printed, not where the machine ends up.

The interesting variation is not "the same program in ten syntaxes" — it is how the model is encoded. Five strategies recur:

All five cite one rule, the canonical scheduling policy. They differ in where the firing order is decided, not in what it is.

FORMS.md specifies each one precisely, including why all five are held to a single golden trace rather than one golden per form.

Thirty-nine programs. The gaps are deliberate:

• generated exists for the four languages tools/codegen targets, plus Solidity. Adding a language means adding one template — see below.
• Solidity has no scheduler and no stdout, so interpreter and lambda have nowhere to land. Contract is the form the language forces on you, which is exactly why it is worth showing. It also cannot model-check itself at startup, so proof has nowhere to land either.
• proof exists everywhere it could be run on this repo's own gates: the four Bazel languages, plus Bash and Lean on the native gate. The Ruby, Julia and Haskell entries are welcome contributions — the spec is in FORMS.md.

Layout is uniform: <lang>/<form> where the language needs directories (Go, Rust) and <lang>/<form>.<ext> where it does not.

make all            # every form in every locally available language
make run-go         # all five Go forms      (also run-rust, run-python, run-js)
make run-bash       # all four Bash forms    (also run-lean)
make run-ruby       # all three Ruby forms   (also run-julia, run-haskell)
make help

Two gates, because two kinds of toolchain:

make parity         # bazel test //... — the 20 in-graph programs, hermetically
make parity-native  # ruby, julia, haskell, bash, lean against the same golden

make parity builds Go, Rust, Python and JavaScript under hermetic toolchains (Go SDK 1.26.0, Rust 1.86.0, Node 22.14.0, CPython 3.12), runs all twenty programs, and diffs each one's stdout against the golden. If any drifts, the build fails and the diff names it. It also runs three artifact gates in //tools/codegen:

parity/reachability.golden is the net's full reachable state space — 16 markings, 26 edges, one terminal marking — with the transitions enabled in each and where they lead.

The trace golden pins one path; this pins the machine. A single trace is equally consistent with a net that never offers a choice, so by itself it cannot tell "these thirty-nine programs agree about this machine" apart from "they agree about one path through a machine none of them has explored". The proof forms in six languages each compute this space privately and throw it away; writing it down once means they can be checked against each other instead of each being trusted on its own.

Pins match the ecosystem-wide line (rules_go 0.61.1 / gazelle 0.51.3 / Go SDK 1.26.0) so compiled actions share cache keys with the other Bazel repos in the Workspace. The shared remote cache is opt-in and read-only by default:

bazel test --config=remote //...     # needs ~/.netrc for bazel.stackdump.com

make parity-native covers what Bazel does not. It runs whichever of ruby/julia/haskell/bash are installed and skips the rest — loudly. A run where everything skipped exits 0 but says NOTHING CHECKED, so a missing toolchain can never masquerade as a pass.

Solidity is in neither gate. There is no hermetic solc here and a contract has no stdout; the event log is the trace, which would need an EVM to observe. Both .sol files compile clean under solc 0.8.24, and the generated one is still covered by the codegen drift test — but nothing asserts their behaviour. That is the one honest gap in the matrix.

model.json is the source of truth for the generated form.

make generate         # regenerate every <lang>/generated from model.json
make check-generated  # fail if any of them is stale

Generated files carry a DO NOT EDIT header and are checked in, so the repo stays readable without running the generator. tools/codegen is a single Go program with one text/template per target language (tools/codegen/templates/); adding a language is one template plus one line in the langs map.

Output is deterministic — places, transitions and arc lists are all sorted by name — which is what makes the drift test possible.

Sorting is also what makes the generated scheduler an implementation of the canonical scheduling policy rather than a coincidence — see below.

Native test suites, where they exist:

cd golang && go test ./...
cargo test --manifest-path rust/Cargo.toml
cd python && PYTHONPATH=. python3 test/main_test.py
cd javascript && npm install && npm test        # mocha; not in the Bazel graph

• Python's lambda form is lambda_form.py because lambda is a keyword.
• Ruby's contract form spells Send as send_order, because Object#send is Ruby's reflection entry point and overriding it on a public API object is a trap.
• Haskell's lambda form is the one that needs no scaffolding: Maybe Marking is "(marking, fired)", and the purity the other languages arrange by copying is free.
• Julia's enum members carry the canonical CamelCase names directly, so string(t) gives the trace spelling with no name table.
• Lean's interpreter form is the only implementation that has to declare it might not terminate: the scheduler loop is partial def, because "runs until no transition is enabled" is a property of this net rather than something the compiler can see. The lambda and contract forms need no such escape hatch — they recurse structurally on a finite schedule. Lean is also the one language here with no set type in scope without pulling in a library, so the marking is a List State; the 1-safe invariant is what makes that honest, and it is checked, not assumed, on every fire.
• The proof form makes that check a theorem. In Go, Rust, Python, JavaScript and Bash it is an exhaustive model-check at startup, every run; in Lean the same breadth-first search runs inside the kernel via decide, and an unsafe net is a compile error — main cannot exist unless 1-safety and the unique {Payment} deadlock hold. See FORMS.md.
• JavaScript's mocha suite needs npm, which does not fit the dependency-free hermetic Node setup, so it stays outside bazel test.

New languages and new forms are both welcome. The bar is the same either way: it must emit the canonical trace, and it must be wired into one of the two parity gates. Start from FORMS.md — it is the spec, not a description.