Alloy

Alloy is the declarative modeling language used for the Arda domain model. The model and its checking recipes live in the manufacturing-ontologies repository; this page covers what its gate does and does not tell you.

For the practice behind reading any gate honestly, see What a Green Run Proves.

What a green gate covers

The check-alloy recipe iterates the model roots and runs the solver over each. Its loop excludes alloy/soak/* and */legacy/* by construction, so a green run says nothing whatever about the soak roots or the legacy models. Those have their own targets and their own verdicts.

This is correct behavior and a misreading waiting to happen. A green check-alloy is evidence about the roots the loop visited. When reporting one, name the roots — or name the exclusions.

Where the verdict comes from

The gate’s verdict rests entirely on the solver’s exit code.

The human-readable output beside it is produced by a grep that ends in || true, so it cannot fail the run. A reader watching that output is watching the half that cannot say no. When a run’s readable summary and its exit status disagree, the exit status is the one that decided.

Concurrent runs corrupt each other’s record, not their verdicts

Instance output and the display log are written to fixed paths shared across seven targets. Two runs in one tree at the same time overwrite each other’s readable output while each run’s own pass or fail remains correct.

The result is a run that is right and a record that is wrong, which is harder to notice than a failure. Give each run its own output path — a run id, a timestamp, a slot name — before running two of anything concurrently in the same tree.

Sources

The gate’s behaviour was read from the manufacturing-ontologies working tree, where the Makefile was uncommitted at the time of writing — so it matches no committed revision, and a reader checking it at ae31cc9 will not find the recipe described. Pin this page to a revision once that file lands.

Stating that rather than citing a plausible ref is the same discipline the craft pages apply: a claim names the corpus it was read from, and an unpinnable source is said to be unpinnable. The submission this page was written from is /workbooks/notebooks/domain-ontology/streams/minesweeper/parmandil-submission-2026-09-09.md.