axon-lang
AXON — the formal cognitive language: a deterministic, proof-carrying AI runtime.
AXON is a programming language for AI cognition in which the properties you care about — this endpoint may not leak regulated data, this agent may not exceed this budget, this credential may not outlive this session — are type errors, checked before anything runs, rather than conventions enforced by code review.
The crate publishes as axon-lang; the library import is use axon::*.
The language reference, the design papers and the full documentation live in the repository README. This page is the crate's landing page: what you get, how to install it, and how to watch it refuse something.
Install
| Requirement | Why |
|---|---|
| Rust 1.95+ | the rust-version of every crate in the workspace |
| a C compiler (MSVC / clang / gcc) | axon-csys is a non-optional dependency and builds C23 kernels via cc |
This installs the axon binary. If the build stops with a cc/linker error
rather than a Rust error, the C toolchain is what is missing.
See it work
Now delete shield: PHIShield from the endpoint and check again:
X app.axon 1 error(s)
error [line 4]: axon-T957 axonendpoint 'Api' carries regulated data
(kappa = {GDPR, HIPAA}) across a trust boundary but declares no `shield:`.
Regulated boundaries require a shield whose `compliance:` covers the type's
kappa — ESK Fase 6.1 coverage rule. […] Declaring the classes on the
endpoint's own `compliance:` does NOT cover them: that list is a label,
the shield is the control that acts on a breach.
axon check exits 1. That is the whole idea: the regulatory property rides on
the type system, so it holds at compile time or it does not hold at all.
What's in the box
One binary, 28 subcommands. The ones you are most likely to reach for:
| Command | Does |
|---|---|
axon check |
lex, parse, type-check — the compliance gate |
axon run |
compile and execute (--tool-mode stub runs with no API keys) |
axon compile |
lower to IR JSON |
axon serve |
run the HTTP / SSE / NDJSON / WebSocket server |
axon dossier · axon audit · axon sbom |
regulatory posture, gap analysis, SBOM |
axon prove · axon verify |
emit and independently check proof objects |
axon fmt · axon fix · axon repl · axon inspect |
the usual tooling |
axon --help lists all of them.
As a library
[]
= "2"
use *;
Building tooling rather than running programs? The compiler frontend — lexer,
parser, AST, epistemic type system, type checker, IR generator — is a separate
crate, axon-frontend, with zero
runtime dependencies. An LSP, a linter or an analyzer should depend on that and
skip the server, database and HTTP stack entirely.
API keys
Only needed to execute flows against real backends — never for axon check,
axon compile, axon dossier, axon audit or axon run --tool-mode stub.
Seven backends are supported (Anthropic, OpenAI, Gemini, Kimi, GLM, OpenRouter,
Ollama); see the repository README for
the environment variables each expects.
License
AGPL-3.0-or-later — see LICENSE. Commercial licensing and the enterprise layer are described in the repository.