# Hale > Concurrent systems language where architecture is mechanically checked: compile-time effect certificates and reachability claims that fail closed on unresolvable indirection. Human-and-LLM authorship is one of four stated design pillars. **Camp:** Verification **Also spans:** Orchestration **Author:** Riley Rook **Implementation language:** Rust **Compilation target:** Native via LLVM; WebAssembly **Licence:** Apache-2.0 **First seen:** May 2026 **Maturity:** working compiler **Site:** https://hale-lang.org **Repo:** https://github.com/hale-lang/hale **hale bench (vs Go, Node, Python):** https://github.com/hale-lang/bench **Agent tooling:** - AGENTS.md - MCP server shipped inside the compiler binary (check, build, test, bus graph, placement, spec search) - LSP with contract-surfacing hover - machine-readable topology artifact with countermodel witnesses (--dump-topology) ## Key idea One primitive — the locus — replaces class, module, actor, and service; loci communicate over a typed topic bus, and the same source runs as a test, a single binary, or a mesh of binaries by editing only the main locus. Contracts scale from per-function effect certificates (@no_syscall, @effects(only:)) to program-wide claims (forbid reaches(A, B)) checked at compile time, with unknown call targets treated as violations and minimal countermodel witnesses on failure. The case for LLM authorship is subtractive: no async colouring, no lifetimes, no lock selection — the shapes models tend to hallucinate aren't in the language. ## The bet. Hale's position is that the distance between how you describe a system out loud and what you type should be near zero — and that the same property that helps a human helps a model. One primitive, the locus, stands in for class, module, package, actor, and service. Loci communicate over a typed topic bus and never reach sideways into each other; a `main` locus declares placement (threads, cores, NUMA nodes) and bindings (in-process queue, Unix socket, shared-memory ring), so deployment shape is an edit to one block, not a rewrite. LLM authorship is one of four stated design pillars, not the whole thesis, and the argument for it is subtractive rather than additive: there is no async colouring, no lifetime annotation, no lock vocabulary, no iterator/closure machinery. The constructs a model is most likely to hallucinate are absent, so a large class of plausible-looking wrong programs does not parse. The verification story is what earns the camp placement. Per-function effect certificates (`@no_syscall`, `@deterministic`, `@budget`, `@effects(only: …)`) are proven transitively through helpers and imported libraries. Above them sit claims: named sentences over the assembled program graph — `forbid reaches(A, B)`, `only edges A -> B { publish T; }`, `count publishers(topic T) <= 1`, allocation bounds on paths — declared in the main locus, evaluated by `hale check` as errors, lowered to zero runtime code. Where the graph cannot be resolved, the checker refuses rather than guesses.

Unknown means violation.

## What it looks like.

topic Metrics { payload: Metric; }

locus DeltaTriage {
    bus { subscribe Tasks as on_task; publish Metrics; }
    fn on_task(t: Task) {
        Metrics <- Metric { n: t.id };
    }
}

group delta_wing = { DeltaTriage };
group gamma_wing = { GammaResearch };

main locus Org {
    claims {
        iso_dg: forbid reaches(delta_wing, gamma_wing);
    }
}

This program fails to check, and the diagnostic returns the route:

claim `iso_dg` violated: `delta_wing` reaches `gamma_wing` —
witness: `DeltaTriage::on_task` -(publishes "Metrics")-> `GammaResearch::on_metric`

The witness is a minimal countermodel in the program's own vocabulary, with secondary diagnostics at the publish site, the subscription, and the destination — the compiler tells you where to edit, not just that you are wrong. The agent tooling ships in the compiler binary itself: `hale mcp` exposes the checker, build, tests, the bus graph, placement, and spec search as MCP tools, and the checked-in AGENTS.md is treated as load-bearing surface rather than documentation garnish. The topology the claims are checked against can be dumped as a versioned JSON artifact and re-checked in CI, so an agent (or a reviewer) can diff the architecture, not just the text. Certain workloads are still outperformed by mainstream languages; the cross-language comparison grid, run by the project on a single machine, is tracked in [hale-lang/bench](https://github.com/hale-lang/bench) with the losses stated alongside the wins. ## Design DNA - **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Same camp, different altitude of contract. Vera discharges per-function requires/ensures with an SMT solver; Hale checks whole-program sentences — reachability, publisher counts, allocation bounds — over the assembled locus graph, without a solver. ## Timeline - **May 2026** — First public release. Locus/bus core, arena-per-locus runtime, GenMC model checking of the runtime's concurrent primitives in CI — against hand-written transcriptions of the primitives rather than the shipping C, a limitation the project's own verification notes tabulate. - **Jun 2026** — v0.9.0: native codegen with static devirtualization, lock-free bus, cross-language benchmark grid. - **Jul 2026** — v0.10.0: last breaking surface change; NUMA-aware placement, live hot code-swap (reperspective), macOS support. LSP, formatter, and doc generator follow in point releases. - **Aug 2026** — v0.12–v0.13: effect certificates made fail-closed end to end; @effects(only:) closed-set contracts. - **Aug 2026** — v0.14–v0.15: claims land — architectural law (forbid reaches, only edges, bound, cover) evaluated by hale check as errors, zero runtime cost; library-tier claims travel with imports. --- HTML version: https://agentlanguages.dev/languages/hale/ Catalogue index: https://agentlanguages.dev/llms.txt Catalogue homepage: https://agentlanguages.dev/index.md