How the parts fit together Diagram

The short answer

• Source is checked and lowered by the pipeline, admitted into a signed certificate, loaded only by the runtime, and every step it takes is chained in the ledger, which feeds the next check

Not shown here

• The language packages, the vendored engines, the network package and the tools poly starts
• later questions cover them
• Connected but out of scope: MCP server, Language server, Workflow server, poly-new, Feedback commands, Signed records

Doctrine

• The semantics is the definition, and every check compares the lowering with it: 04-semantics defines what a program means; translation validation runs the lowered module and poly-ref on every reachable state and refuses any disagreement

How the parts fit together

What are the parts of poly, and which way does a program travel through them?

poly has to be believable at two moments: when a person decides to trust a program, and when that program runs. The design answers both with one artefact, the certificate, and one record, the ledger. The tension is that the checker, the compiler and the runtime are all code, and only one of them is allowed to decide.

The long read

Everything starts at the poly CLI, whose command registry the MCP server re-exports, so an agent and a person reach the same commands.

The Check pipeline takes a source file through parse, type, lower, strict validate, translation validation, model check and the later stages. It writes the lowered files into the Certified build and folds every stage verdict into one report. poly-ref sits beside the pipeline and is the part that compares the lowering with the semantics.

Admission is a separate step. It refuses unless every check ran and came out clean, then signs a certificate over the digests of the source and each artefact. The runtime loads only what that certificate names and refuses any file whose digest differs.

At run time the Effect worker takes each effect from the outbox, passes it through the gate and a handler, and the Ledger records the step and the gate's decision in one transaction. The Feedback commands read that ledger back as traces, so what ran can become the next rule, workflow or calibration.

Terms used here

artefact: A file produced by lowering a machine, such as the contract, the SAM v2 module or the effects manifest. The engines read artefacts and never the source.
certificate: A signed record that binds a program's source and artefact digests to the checks that ran and their results. The runtime loads only what one names.
translation validation: Running the lowered module and poly-ref's reading of the semantics on every reachable state, and refusing any difference between them.
poly-ref: poly's own model checker. It is written from the semantics and shares no code with the compiler.
gate: The two-phase mediation of an effect: propose before the call, settle after it. The Polyaxion engine decides allow, deny or escalate.
outbox: The table in which a step leaves its effect intents. The effect worker takes them out one at a time, at least once.
ledger: The record of every step, advice, decision, outcome, gate verdict and effect of a run, hash-chained per run with signed heads and a periodic anchor.
vacuous: A property whose antecedent is never true where it is judged. It holds for no reason the program gives, so it is INCONCLUSIVE and never CLEAN.
vendored engine: An engine file copied unchanged into vendor/ and pinned by hash and commit, so poly relies on the Poly stack conceptually and not physically.
idempotency key: A value sent with a write so that the receiver can recognise a retry of the same request and do the work once. In poly it is the intent id, and the runtime sets it.