/proof

What is checked, and what comes back when it fails

Each property below is checked as an error. A property that is false gets a witness back from the compiler, the concrete path that breaks the rule, in your own names: the call, the route, and the places you would edit.

who checks	what	how
compiler	Typed bus topology	Topic declarations fix the payload type and the publish and subscribe authority. The compiler inspects the closed-world graph for orphaned subjects, impossible handlers, routing-policy errors and re-entrant cycles.	bus →
compiler	Effect reachability	`@no_syscall`, `@no_block`, `@deterministic` and `@budget` are checked across reachable calls, imported seeds, handles and interface dispatch.	effects →
compiler	Causal bus contracts	`causes:` follows outward influence across publishes. `depends:` walks backward through subscriptions and republishers to check the complete set that may reach a locus over the bus graph, including through a republisher in another library. Influence that travels outside the bus is not part of that closure.	causality →
compiler	System claims	Groups name the domains; the main locus states the law: `forbid reaches`, `only edges`, `require`, `cover`, `count`, interposition with `avoiding`, and capability bounds. Violations are errors with countermodels, and the checked model exports as a diffable artifact under a shape hash.	claims →
compiler	One claimset, many worlds	A claim is evaluated in a closed world, so law used to be copied into every entry point. A `constitution` moves the authorship without moving the evaluation: each adopting main still proves it in its own world. Composition only adds. Identity follows the normalized closure, so a shared name is not mistaken for a shared claimset.	constitutions →
compiler	Across binaries	Sealed application artifacts compose into one deployment model. A plan names deployed instances and the routes between them, and law that no single binary can state is checked over the arrangement. Composition takes artifacts, never merged source. Matching wire identities establish compatibility, and only an explicit route creates an edge.	binaries →
compiler	State a caller cannot reach	A locus marked `@sealed` keeps its params to itself: others may call it and cannot read or write it. Loci are not otherwise encapsulated at the field level, so this is what makes confinement a fact the compiler knows. The library's key holders take the name of a source and never the bytes, so no line of application code holds the material. The check covers confinement and leaves information flow out: a value derived from the key is not tracked, and a constant-time compare still lets the verdict be published. Both limits are stated in the specification.	secrets →
runtime + compiler	Structural lifetime	Loci own regions and children. The compiler enforces the managed-entity rules; the runtime dissolves the owned structure deterministically and reports residency when growth needs inspection.	memory →
runtime	Supervised failure	Lifecycle failures travel to an owning parent. A binding that fails to start refuses birth, so no route is installed that accepts and drops messages.	failure →
ci	Concurrent substrate	Models of the runtime's synchronization protocols are model-checked under permitted thread interleavings in CI. This narrows the trusted base beneath queues, mailboxes, maps and arenas, without emptying it.	the models →

The diagnostic names the call path.

A hard rule is useful only when a rejection shows how the forbidden behaviour became reachable.

hale checkeffect witness

effect assertion violated:
  price must not reach syscall

reachable path:
  price
  -> Book.price_for
  -> Book.reload
  -> std::io::fs::read_file

The path continues through the broker.

Local inspection cannot see a dependency hidden behind a republisher. The bus graph can, and the witness names every step.

hale checkdependency witness

declared dependency set violated:
  StatedCarry can transitively depend on SumLookup

Path:
  subject SumLookup
  -> Launderer
  -> subject Recalled
  -> StatedCarry

The law names its countermodel.

A claim quantifies over every represented path. A graph that escapes its declared law gets a diagnostic with the route, calls and message hops, that makes the sentence false.

hale checkclaim witness

claim `iso_dg` violated:
  `delta_wing` reaches `gamma_wing`

witness:
  delta::Triage::on_task
  -(publishes "org.metrics")->
  gamma::Research::on_metric

The path is named across binaries.

The same sentence, one scale out. Each component checked clean on its own; the arrangement did not. The witness crosses artifacts and names every hop, the route that carries it, and the file each vertex lives in, because a deployment defect is only actionable if it says which config and which source to open.

hale fleet checkfleet witness

fleet claim `orders_pass_oms` violated — witness:
  prober-0::Probe::submit  [prober/main.hl]
  -(route `intent`)->
  oms-0::Oms::on_intent  [oms/main.hl]
  -(route `bypass`)->
  gw-0::Gateway::on_order  [gw/main.hl]

The four answers a check can give

ProvenThe build may continue.

ViolatedFail, with a witness.

UnknownFail closed, for a hard contract.

UnsupportedSay exactly what cannot be checked.

The checks ship with the language.

The command line, editor integration, CI and the MCP server all read the compiler's structured diagnostics. The quickest evaluation is to run the examples and make the compiler disagree with you.

toolchaincommands

hale check .
hale check . --dump-topology
hale test .
hale verify .
hale bench .
hale doc --stdlib
hale lsp
hale mcp

What stays in the trusted base

Each *_model.c under verification/ is a hand-written transcription of one synchronization protocol, stripped to its atomics. GenMC explores those models across permitted interleavings on every substrate CI run, so a violation of the synchronization logic is caught. What it does not do is check the transcription against the C it was transcribed from. Correspondence is maintained by hand, and a model that still passes proves a property of the runtime as it stood when the model was written.

The repository's own audit is the inventory, and it is public: which atomics postdate their model, which primitive verifies only under sequential consistency and reports a use-after-free under the release-acquire model that matches the runtime's orderings, and which code paths are not transcribed at all. The claim is about the models alone until drift is detected mechanically and that counterexample is resolved.

The verification audit, including its gaps →

Compile time certifies the structure. Runtime measures the world.

Proven before it runs

Reachability, topology, causality, cardinality, confinement and bounds, over every path in the closed world, including the ones no test takes.

Measured while it runs

Birth, dissolve, publish, delivery and transport evidence, emitted by the observation plane and read against the same model the compiler certified.

Carried between them

The topology artifact: a byte-reproducible record of the checked model, signed and attested, so the fleet that runs is the fleet that was certified.

The verification chapter specifies the analysis boundary: what closed-world reasoning covers, and where a budget is a source-level bound.