Well-formedness checking for Synolon programs: the per-process machine rules of doc/synolon.md §4 — signal-guardedness (the goto-only subgraph of the block graph is acyclic), representability (every binder, block parameter, cell, port, and halt answer has a fixed bit width, by ReWire.Synolon.Repr), block normal form (command right-hand sides are simple computations; terminator operands and put payloads are atoms or primitive expressions), cell-initial constness and typing, full-arity pauses and gotos, the resumed-input parameter rule, and "the process pauses" — over the expression-level checker of ReWire.Eidos.Lint at mono+ANF strength with the reactive types out of the type grammar, plus the program rules: name distinctness, global uniqueness over the datatype-and-definition fragment, the definition rules on the definitions the machine calls, and pure-acyclicity (the call graph of the definitions reachable from a process is acyclic, and no recursive let is reachable).

Process binding sites are scoped, not globally unique: purify splices one definition per continuation and passes one binder along goto chains, so a unique is legitimately bound by several blocks. Labels and cells are distinct per process; within a block every binding site is distinct and disjoint from the definition-level sites; and in-block binding is validated by scoping and occurrence-signature agreement.