axon-lang 4.0.0

AXON — the formal cognitive language: a deterministic, proof-carrying AI runtime. Native Rust lexer/parser/type-checker/IR generator (re-exported from axon-frontend) plus the runtime: typed channels (π-calculus mobility, capability extrusion), algebraic effects via Free Monad CPS handlers, lease kernel + reconcile loop, the Epistemic Security Kernel, Trust Types, Proof-Carrying Code (independently verifiable proof objects), and the closed-catalog extension mechanism. Crate publishes as `axon-lang`; library import is `use axon::*` so existing call sites keep working unchanged.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158

# axon-lang


**AXON — the formal cognitive language: a deterministic, proof-carrying AI runtime.**

[![crates.io](https://img.shields.io/crates/v/axon-lang.svg)](https://crates.io/crates/axon-lang)
[![docs.rs](https://docs.rs/axon-lang/badge.svg)](https://docs.rs/axon-lang)
[![License: AGPL-3.0-or-later](https://img.shields.io/badge/license-AGPL--3.0--or--later-blue.svg)](https://github.com/VelitRicardo/axon-lang/blob/master/LICENSE)

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](https://github.com/VelitRicardo/axon-lang).** 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` |

```bash
cargo install axon-lang
```

This installs **`axon`** — the compiler and governance CLI. It is what you want
in CI, in a pre-commit hook, and on a developer machine: `axon check` needs no
database, no HTTP server and no API key.

If the build stops with a `cc`/linker error rather than a Rust error, the C
toolchain is what is missing.

### Running governed flows: `axon-server`


`axon` compiles and audits; **`axon-server` executes**. It is a separate binary
behind a feature flag, the way `psql` and `postgres` — or `docker` and `dockerd`
— are separate:

```bash
cargo install axon-lang --features server            # adds `axon-server`
cargo install axon-lang --features server,postgres   # …with the SQL data plane
```

| feature | adds |
| ------- | ---- |
| *(none — the default)* | `axon`: check, compile, run, dossier, audit, sbom, prove, verify, fmt, fix, repl, … |
| `server` | the `axon-server` binary — HTTP / SSE / NDJSON / WebSocket |
| `postgres` | `backend: postgresql` axonstores, `axon store introspect` |
| `documents` | the OOXML surface (§99/§100/§106) and `axon evidence-package` |

**Both binaries are AGPL and both live in this crate.** The split is a *role*
boundary — compiler vs runtime — not a paid one.

Nothing disappears when you install less. **Every subcommand stays in `--help`
under every profile**, and one whose feature is absent refuses in writing with
the exact command that brings it back:

```
$ axon serve
X `axon serve` requires the `server` feature - this build was compiled without it…
  Reinstall with: cargo install axon-lang --features server
  and run `axon-server` (the `axon` you have keeps working for everything else).
```

`axon check` type-checks a program that declares `backend: postgresql` even in a
build with no database driver — the compiler resolves a *declaration*; it opens
no connection.

**What the split costs and buys** (measured 2026-08-06, warm registry, cold
target dir): the default install is **11m09s → 7m05s** and the `axon` binary
**36.1 MiB → 19.1 MiB**.

## See it work


```bash
echo 'type PatientRecord compliance [HIPAA, GDPR] { ssn: String }
shield PHIShield { scan: [pii_leak] on_breach: halt severity: critical
                   compliance: [HIPAA, GDPR] }
axonendpoint Api { method: POST path: "/p" body: PatientRecord
                   execute: F output: FlowEnvelope<PatientRecord> shield: PHIShield
                   backend: anthropic compliance: [HIPAA, GDPR] }
flow F(ssn: String) -> PatientRecord {
  step R { ask: "summarize" output: PatientRecord } }' > app.axon

axon check   app.axon                  # compile-time compliance verification
axon dossier app.axon                  # regulatory posture, as JSON
axon audit   app.axon --framework all  # per-framework gap analysis
```

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


**28 subcommands, all of them listed under every profile.** 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 — needs `--features server`, and points you at `axon-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


```toml
[dependencies]
axon-lang = "2"
```

```rust
use axon::*;
```

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`](https://crates.io/crates/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](https://github.com/VelitRicardo/axon-lang) for
the environment variables each expects.

## License


AGPL-3.0-or-later — see
[LICENSE](https://github.com/VelitRicardo/axon-lang/blob/master/LICENSE).
Commercial licensing and the enterprise layer are described in the
[repository](https://github.com/VelitRicardo/axon-lang).