A check, in order Diagram

The short answer

• The pipeline parses and lowers the machine, has sam-pattern validate it, has poly-ref compare it with the semantics, and only then lets polygraph explore it, with poly-ref confirming what polygraph finds

Not shown here

• Effects, composition, configuration and policy stages, which run after these for machines that have them
• Connected but out of scope: MCP server, Language server, Workflow server, poly-new, Admission, Feedback commands

What it guarantees

• A check that did not run or hit a bound is never CLEAN: the verdict fold ranks INCONCLUSIVE and UNDERPOWERED apart from CLEAN, vacuous properties are INCONCLUSIVE, and admission refuses a build with any check not run

A check, in order

What happens, in order, when poly check runs on a machine?

A check has to be cheap to trust. The pipeline's order is the argument: no engine explores a module that poly-ref has not already shown to mean what the source says, so a finding from an engine is a finding about the program and not about the lowering.

The long read

The CLI hands a target to the pipeline. Stage 0 parses the source with poly-lang and runs the type and domain checks in poly-core. A refusal here stops the machine and the later stages are listed as not run, with the reason.

A checked machine is lowered. sam-pattern then validates the lowered module against the strict profile. Only after that does poly-ref run translation validation: it executes the lowered module and its own reading of the semantics on every reachable state and refuses any difference (PL2501).

Now polygraph explores the module for invariants. Its findings are not taken on its word. The pipeline asks poly-ref to confirm each witness against the checked instance, and a finding that leaves the instance becomes a bound hit and not a finding. poly-ref also decides deadlock freedom and liveness, which no engine checks.

The report returns to the CLI with a verdict, the diagnostics and witnesses. A stage that did not run is listed as not run and never lowers the verdict.