Typed bus topology
Topic declarations establish payload type and publish/subscribe authority. The compiler inspects the closed-world graph for orphaned subjects, impossible handlers, routing-policy errors, and re-entrant cycles.
Bus semantics →proof
What the compiler certifies, and the witness it hands back.
Each rung of the structure closes at a different scale, and each one is checked as an error rather than a suggestion. When a property is false, the answer is a countermodel in your own spelling: the path, the route, and the three places you would edit.
Effect reachability
Assertions such as @no_syscall, @no_block, @deterministic, and @budget are checked across reachable calls, imported seeds, handles, and interface dispatch.
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.
System claims
Groups name the domains; the main locus states the law: forbid reaches, only edges grants, require/cover/count, interposition via avoiding, and capability bounds. Violations are errors with countermodels, and the checked model exports as a diffable artifact under a shape hash.
One claimset, many worlds
A claim is evaluated in a closed world, so law used to be copied into every entrypoint. A constitution moves the authorship without moving the evaluation: each adopting main still proves it in its own world. Composition only ever adds: a stricter rule is a second clause, never a replacement, and identity follows the normalized closure, so a shared name is not mistaken for a shared claimset.
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, every order path crosses risk, exactly one deployed publisher, is checked over the arrangement. Composition takes artifacts, never merged source: matching wire identities establish compatibility, and only an explicit route creates an edge.
Across binaries →State a caller cannot reach
A locus marked @sealed keeps its params to itself: others may call it, not read or write it. Loci are not otherwise encapsulated at the field level, so this is what makes confinement a fact the compiler knows rather than one you verify by reading. The library's key holders take the name of a source rather than the bytes, so no line of application code holds the material.
The law is then ordinary: one classified operation, and claims that say who may reach it and how often. Two verbs quantify over the whole program rather than a path, every locus in a group confined, every boundary crossing naming a purpose, so code written next month is covered without editing the claim.
Confinement, not information flow: 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.
Confine, classify, claim →Structural lifetime
Loci own regions and children. The compiler enforces managed-entity rules; the runtime dissolves the owned structure deterministically and reports residency when growth needs inspection.
Memory and lifetime →Supervised failure
Lifecycle failures travel to an owning parent. Binding startup failures refuse birth instead of installing a route that silently accepts and drops messages.
Failure and supervision →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.
What the models do and do not establish →operational witness
The diagnostic names the call path.
A hard rule is useful only when a rejection shows how the forbidden behavior became reachable.
hale check
effect assertion violated:
price must not reach syscall
reachable path:
price
-> Book.price_for
-> Book.reload
-> std::io::fs::read_filehale check
declared dependency set violated:
StatedCarry can transitively depend on SumLookup
Path:
subject SumLookup
-> Launderer
-> subject Recalled
-> StatedCarryarchitectural witness
The path continues through the broker.
Local inspection cannot see a dependency hidden behind a republisher. The bus graph can, and the witness should name every step.
system witness
The law names its countermodel.
A bundle-level claim quantifies over every represented path. When the assembled graph escapes its declared law, the diagnostic returns the route, calls and message hops, that makes the sentence false.
hale check
claim `iso_dg` violated:
`delta_wing` reaches `gamma_wing`
witness:
delta::Triage::on_task
-(publishes "org.metrics")->
gamma::Research::on_metricdeployment witness
The path is named across binaries.
The same sentence, one altitude up. Each component checked clean on its own; the arrangement did not. The witness crosses artifacts, naming 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 check
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]reproduce it
The checks ship with the language.
The command line, editor integration, CI, and MCP server all use the compiler's structured diagnostics. The quickest evaluation is to run the examples and make the compiler disagree with you.
toolchain
hale check .
hale check . --dump-topology
hale test .
hale verify .
hale bench .
hale doc --stdlib
hale lsp
hale mcpwhat stays in the trusted base
The model is a transcription, and that is a boundary.
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 honest 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. Until drift is detected mechanically and that counterexample is resolved, the claim is about the models, not about the runtime by implication.
The verification audit, including its gaps →the division of labor
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, not the ones a test happened to take.
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.