Cortex Usage Guide

Practical guide for installing Cortex, writing a first Wire workflow, running Pulse, and deploying a consumer-bound runtime.

On this page
  1. The Working Model
  2. Reading Path
  3. What This First Pass Covers
  4. What Is Proven
  5. Related

Cortex Usage Guide

This chapter is for people who want to use Cortex before they study its architecture.

Cortex has three practical jobs:

  1. Write workflow topology in Wire.
  2. Bind that topology to registered executors.
  3. Run the compiled circuit with Pulse.

You do not need the graph algebra or Lean proof story to start. Those explain why the substrate is shaped the way it is. This guide starts with the working path and links to the deeper material only when it matters.

The Working Model

.wire source
  -> compiled circuit
  -> Pulse task definition
  -> durable run state
  -> events, outputs, checkpoints, and provenance

Wire is the authoring language. Pulse is the durable runtime. A host or consumer library provides the executor registry that gives node bodies their authority.

The stock cortex-pulse binary is intentionally a substrate shell with an empty task registry. It is useful for checking the runtime surface and health behavior. Real deployments usually link Cortex from a consumer repo and pass a populated registry to Cortex.Pulse.runPulse.

Reading Path

If you want to…Start with
Build the repo and see the surfacesQuickstart
Understand the shape of a Wire fileYour first Wire workflow
Learn what Pulse needs at runtimeRunning Pulse
Prepare an operator-facing serviceDeploying Pulse
Embed Cortex in another Haskell repoIntegrating from Haskell
Diagnose common failuresTroubleshooting
Check proof and correspondence statusProof status
Look up exact syntax or schemasReference
Understand the design commitmentsArchitecture overview

What This First Pass Covers

This Usage chapter is intentionally a light working guide. It deliberately avoids becoming the Wire book. Writing Wire deserves its own teaching sequence because the language has nodes, ports, contracts, CorePure expressions, executor authority, configured executor values, signals, and rewrites. The Usage chapter should teach the shortest operational path; the Wire book should teach the language properly.

What Is Proven

Cortex has a machine-checked proof surface for graph safety, fixed-topology Pulse safety, CorePure evaluation boundaries, node ingress/body/egress normal form, rewrite admission, and selected-branch actualization. The proof status dashboard separates those Lean claims from Haskell implementation correspondence so you can see which guarantees are closed, hooked, or still open.