Axiom

A small, embeddable policy engine for AI agents. Write a policy file, check intentions before execution.

Think SQLite — not a server, not a framework, just a library you drop in.

Your agent can say anything. It can only do what policy allows.

---

The Problem

MCP servers enforce policy at the routing layer. But agents with native OS-level tools — bash, file system access, shell — bypass MCP entirely and run commands directly. The policy server never sees them.

Axiom operates at the conscience layer — inside the agent's decision loop, before anything executes. It doesn't matter how the agent reaches execution. If the intent violates policy, it's blocked.

MCP policy + Axiom = full coverage. Each guards what it can see.

---

Quick Start

Download pre-built binaries:

# Linux
wget https://github.com/latentcollapse/Axiom/releases/latest/download/axiom-linux-x64.zip
unzip axiom-linux-x64.zip
# You now have: libaxiom_lang.so, axiom.h, examples/

# Windows
# Download axiom-windows-x64.zip from releases
# Contains: axiom_lang.dll, axiom.h, examples/

Or build from source:

git clone https://github.com/latentcollapse/Axiom
cd Axiom
cargo build --release
# Output: target/release/libaxiom_lang.so (or .dll on Windows)

---

Use It

C (or any language with C FFI):

#include "axiom.h"

int main() {
    axiom_engine_t *eng = axiom_engine_open("policy.axm");

    const char *keys[] = { "path" };
    const char *vals[] = { "/tmp/output.txt" };
    int rc = axiom_verify(eng, "WriteFile", keys, vals, 1);

    if      (rc == 1) puts("allowed");
    else if (rc == 0) printf("blocked: %s\n", axiom_denied_reason(eng));
    else              printf("error: %s\n",   axiom_errmsg(eng));

    axiom_engine_close(eng);
}

Compile:

gcc main.c -L. -laxiom_lang -o myapp

Rust:

# Cargo.toml
[dependencies]
axiom-lang = { git = "https://github.com/latentcollapse/Axiom" }

use axiom_lang::AxiomEngine;

let engine = AxiomEngine::from_file("policy.axm")?;
let verdict = engine.verify("WriteFile", &[("path", "/tmp/output.txt")])?;

if verdict.allowed() {
    // proceed
} else {
    eprintln!("blocked: {}", verdict.reason().unwrap_or_default());
}

Python:

pip install axiom-lang

from axiom import AxiomEngine

engine = AxiomEngine.from_file("policy.axm")
v = engine.verify("WriteFile", {"path": "/tmp/output.txt"})

if v.allowed:
    print("allowed")
else:
    print(f"blocked: {v.reason}")

---

Write a Policy

module security {
    intent WriteFile {
        takes: path: String, content: String;
        gives: success: bool;
        effect: WRITE;
        pre: !contains(path, "/etc/");
        pre: !contains(path, "..");
    }

    intent ReadFile {
        takes: path: String;
        gives: content: String;
        effect: READ;
        pre: !contains(path, "/etc/shadow");
        pre: !contains(path, ".ssh/");
    }

    intent RunCommand {
        takes: command: String;
        gives: output: String;
        effect: EXECUTE;
        pre: !contains(command, "rm -rf");
        pre: !starts_with(command, "curl");
        conscience: no_bypass_verification;
    }
}

Save as policy.axm, load it, verify intentions. Done.

---

Conscience Predicates

This is where Axiom differs from rule engines.

Standard policy engines match patterns against blocklists. Conscience predicates are structural invariants — properties the engine proves hold before execution, not patterns it hopes to match. An agent can't route around them by rephrasing the command.

Three built-in predicates, formally verified with Rocq/Coq (see axiom rocq proofs/):

Predicate	Blocks
path_safety	/etc/shadow, .ssh/, path traversal (../..)
no_exfiltrate	Network writes to undeclared destinations
no_bypass_verification	Execute-class intents carrying unverified external data

Add them to any intent:

intent RunCommand {
    takes: command: String;
    effect: EXECUTE;
    pre: !contains(command, "rm -rf");
    conscience: no_bypass_verification, path_safety;
}

The Rocq proofs (axiom rocq proofs/G1_Purity.v through G6_Totality.v) formally verify the six core correctness properties of the conscience kernel — purity, effect classification, determinism, monotonic ratchet, specific denial, and totality. The proofs compile clean with coq_makefile.

---

Inference Modes

Three enforcement levels, selectable at runtime:

Mode	Behavior
Flow	Maximum inference — fills in implicit constraints, minimum verbosity
Guard	Default — trust-explicit, blocks anything not declared
Arx	Strict — everything not explicitly permitted is denied

All modes compile to identical Arx-equivalent under the hood. Flow and Guard are syntactic convenience; the safety guarantees are the same.

---

Pre-Conditions

The pre: field defines what's allowed:

Function	Example	Meaning
contains(s, sub)	contains(path, "/tmp")	String contains substring
starts_with(s, prefix)	starts_with(cmd, "nmap")	String starts with prefix
matches(s, pattern)	matches(url, "https://.*\.internal\.com")	Regex match
length(s) > N	length(content) < 10000	Length comparison
!	!contains(path, "..")	Negation
&&, ||	pre: a && b	Combine conditions

All pre-conditions must pass for an intent to be allowed.

---

API Reference

Function	Returns
axiom_engine_open(path)	Handle to engine
axiom_engine_open_source(src)	Handle from string
axiom_verify(eng, intent, keys, vals, n)	1=allowed, 0=denied, -1=error
axiom_denied_reason(eng)	Why it was blocked
axiom_errmsg(eng)	Error message
axiom_engine_close(eng)	Free handle
axiom_version()	Version string

---

Building

cargo build --release   # libaxiom_lang.so / .dll / .dylib
cargo test              # run test suite

Requires Rust 1.70+. Only dependency is blake3.

To verify the Rocq proofs:

cd "axiom rocq proofs"
make
# All six G-proofs + AxiomTypes + AxiomVerify + Concrete should compile clean

---

Status

MVP. Core verification works. Pre-conditions, conscience predicates, C/Rust/Python bindings, three inference modes, and formal Rocq proofs all functional.

The API will evolve. Breaking changes may occur before 1.0.

Use it, test it, break it. Issues and PRs welcome.