🟢 Live demo — verify a capability with the real compiled kernel, right in your browser
A capability gate between any decision and any real-world action.
If an agent, planner, or service wants to read a file, call an API, or move money, AuthGate checks one structural question first:
Does this actor hold a valid, signed, non-revoked capability for this resource and these rights?
No valid proof → the action does not run. Same inputs always yield the same Permit or Deny. No LLM calls inside the gate. No probability scores.
Not a LangChain plugin. Not model-specific. The product is a wire format plus a verify function. Framework adapters are convenience glue — when a framework goes away, the contract stays. See POSITIONING.md.
Constitution (book + philosopher edition): Aliipou/freedom-theory. This repo is authority (AuthGate TCB). It does not replace the legitimacy floor. Start there for A1–A7; start here for signed capability proofs.
Deployable verifier API: INFRA.md — Docker Compose, /readyz, admin-gated registry mutation, attenuating /delegate.
flowchart LR
D[Decision maker] --> G[CallGate / AuthGate]
G -->|Permit| IO[Tool / IO]
G -->|Deny| A[Hash-chained audit]
Review / ops: REVIEW_PACKET.md · ASSUMPTIONS.md · INFRA.md · INDUSTRY_READINESS.md
Engineering gap audit — closed. All items from the original gap list are resolved or explicitly scoped (see Engineering gaps). No open rows remain.
CI — all green on branch with-legitimacy (PR #8 → main):
| Workflow | What it verifies |
|---|---|
| CI | Rust clippy/tests, Python ruff/mypy/pytest, docker /readyz, red-team, adversarial simulation |
| Formal verification | TLC model check + Lean 4 lake build (FreedomKernel) |
| Seccomp enforcement | Linux adversarial: execve killed under read-only allowlist |
| Sandbox | WASM sandbox: write blocked with read-only rights |
| TCB Test Suite | Full Rust TCB regression |
New enforcement & ops modules:
authgate-kernel/src/seccomp.rs— rights-derived syscall allowlist (mirrors WASM bitmask)authgate-kernel/src/session_clock.rs— monotonic session clock; rejects backward time jumpstests/test_seccomp_adversarial.py— seccomp kill-test in CI
Formal system posture (honest): minimal, incomplete but consistent — every theorem is proved, admitted (sorry), or listed as axiom/non-goal. Security-critical scope lemmas T-SC3/T-SC4 are proved; 2 sorry remain in Scope.lean (trailing /, prefix antisymmetry); 2 crypto axioms in Proofs.lean. Details: formal/INCOMPLETENESS.md.
Industry readiness tiers defined in INDUSTRY_READINESS.md — T1 assurance-bounded through T4 production infra-ready. Current branch meets T2 engineering-complete (gaps closed + CI green); ops guides (KMS, DR, migration) land in T3/T4 docs.
Pending: merge PR #8 to main so the default branch carries the same CI and gap closure.
Autonomous systems increasingly decide and act. The decision step (LLM, planner, workflow) can propose tool calls faster than humans can review them. Most stacks still treat “the agent asked for it” as enough authority.
That leaves a predictable failure mode: an actor executes IO without a cryptographically checkable proof that it was allowed to. Prompt framing, framework bugs, or a compromised sub-agent should not be able to invent authority.
AuthGate puts a small, deterministic gate on that arrow:
[Any decision-maker] → CallGate (verify capability proof) → [Any IO]
↓ if denied
audit entry; action does not execute
Today the decision-maker is often an LLM agent. Tomorrow it may be a planner, a swarm, or another machine. The gate does not care — it only checks the proof.
| Capability | What it means in practice |
|---|---|
| Signed capability chains | Ed25519-signed proofs; identity bound as subject_id = SHA-256(pubkey) |
| Attenuation | A child can only receive a subset of a parent’s rights — never amplify |
| Epoch revocation | Raise min_epoch to invalidate a compromised cohort in O(1); no giant denylist required |
| Deterministic decisions | Same action + same trust root + same time → same Permit/Deny |
| Tamper-evident audit | Hash-chained log of gate decisions |
| Small Rust TCB | Security-critical path is a few hundred LOC with #![forbid(unsafe_code)] |
| JSON wire contract | Integrate by producing/consuming schemas — no framework lock-in |
| Partial formal coverage | TLA+ model checked (safety), Kani harnesses, Lean 4 theorems — see honesty section below |
Wire schemas (the integration contract):
spec/canonical_action.schema.json— what you submitspec/gate_result.schema.json— what you receivespec/audit_entry.schema.json— what gets logged
Adapters for LangChain, OpenAI Agents SDK, Anthropic, AutoGen, CrewAI, LangGraph, DSPy, and MCP live under src/authgate/adapters/ as optional conveniences, not as the product.
This is the same family of idea as capability-based OS security (seL4, CHERI), applied to agent tool execution rather than to syscalls.
AuthGate is not “a better OPA.” General policy engines already answer “is this principal allowed to do this action on this resource right now?” Cedar is formally verified as a policy language; Zanzibar / OpenFGA scale relationship-based access; OPA’s Rego is highly expressive. We do not claim to replace those systems for service mesh, cloud IAM, or classic ABAC.
What we do claim, based on a written comparative evaluation (COMPARATIVE_EVALUATION.md, kill-tests in WHY_NOT_OPA.md / WHY_NOT_DLP.md):
| System | Strength | Gap relative to agent tool gates |
|---|---|---|
| OPA / Rego | Flexible policy language for services | Not built around signed capability delegation chains; formal verification of the interpreter is not the product story |
| AWS Cedar | Formally verified authorization language | Point-in-time allow/deny; no agent-oriented capability DAG + epoch cohort revoke as first-class primitives |
| Zanzibar / OpenFGA | Global ReBAC; revocation via tuple delete | Excellent relationship graphs; not a per-tool-call capability proof + attenuation lattice for agent runtimes |
| DLP / lineage / PBAC | Catch sensitive content at egress or purpose at query time | Usually outside the agent loop; do not bind “obtained under capability C” to later tool sinks |
| Object-capability OS (Capsicum, EROS) | Strong confinement theory | Process/OS layer — not a portable JSON gate for LLM tool calls |
| Sandboxes (gVisor, Firecracker) | Isolate processes/VMs | Isolation ≠ typed authority for which agent action may run |
AuthGate’s practical niche: a small, auditable authority check at the agent↔tool boundary — signed proofs, attenuation, epoch revoke, hash-chained decisions — with a path toward purpose/flow controls layered on capabilities. That is narrower than “replace enterprise IAM,” and stronger than “another LangChain middleware.”
If you only need Rego policies for a REST API, use OPA. If you need relationship tuples at global scale, use OpenFGA. If you need a capability gate in front of agent tools with cryptographic proofs and a tiny verified core, evaluate AuthGate.
| Not this | Why |
|---|---|
| Model alignment / ethics | Values and intent need semantics; this gate is structural |
| Natural-language intent parsing | The kernel does not interpret prompts |
| Side-channel defense | Timing and covert channels are out of scope (THREAT_MODEL.md) |
| Python as the security boundary | src/authgate/ is a compatibility runtime — bypassable; only the Rust TCB carries the security claims |
| Perfect formal completeness | Partial proofs and bounded model checking — not a full refinement proof from TLA+ to Rust |
Full gap list: formal/INCOMPLETENESS.md. Assumptions that must hold for claims to apply: ASSUMPTIONS.md.
Optional philosophy / Theory-of-Freedom notes live under PHILOSOPHY/ and FREEDOM_THEORY_POSITION.md. They are not the industrial claim and do not expand the TCB.
| Metric | Value |
|---|---|
| Security-enforcing Rust path | engine.rs + dag.rs + call_gate.rs — on the order of a few hundred LOC |
| Rust crate lib tests | ~293 (cargo test --lib) |
| Python / integration tests | 1300+ passing |
| Kani harnesses | 19 proved (bounded) |
| Lean 4 | Partial — TCB/Temporal/MultiAgent proved; Scope: 2 sorry; 2 crypto axioms |
| TLA+ / TLC | Safety model checked; CI-verified via formal.yml (formal/tlc_run.log) |
| CI workflows (PR #8) | 5/5 green (CI, Formal, Seccomp, Sandbox, TCB) |
Python verify() latency (indicative) |
p50 ≈ 10–17 µs depending on registry size |
Treat formal badges as evidence of engineering discipline, not as a certificate that every deployment is secure. Crypto implementations and clock integrity remain caller/environment responsibilities unless separately attested.
Human principal (trust root)
│ signs CapabilityProof chains; sets min_epoch to revoke
▼
CanonicalAction (actor, resource, rights, proofs, nonce, binding_hash)
▼
CallGate — binding → identity → expiry → epoch → resource → attenuation → revocations
▼
Decision::Permit | Decision::Deny { reason }
▼
AuditLog (SHA-256 hash-chained)
Identity binding: every delegation node must satisfy subject_id = SHA-256(issuer_pubkey). Knowing a parent proof hash without the private key is not enough to forge a child.
Revocation: advance min_epoch on actions; proofs below that epoch fail. Cohort kill without maintaining a long revocation list.
Nine TCB invariants (binding, identity, expiry, epoch, resource, attenuation, chain epoch/completeness, revocation safety) are listed under Security invariants.
cp .env.example .env # set AUTHGATE_ADMIN_TOKEN
docker compose up --build -d
curl -s localhost:8000/readyzDetails: INFRA.md.
use authgate_kernel::tcb::{
call_gate::CallGate,
types::{CanonicalAction, Decision, RIGHT_READ},
};
let gate = CallGate::new(root_verifying_key);
let mut action = build_canonical_action(/* ... */);
action.binding_hash = action.compute_hash();
match gate.execute(&action, unix_now()) {
Decision::Permit => execute_action(),
Decision::Deny { reason } => reject(reason),
}from authgate.kernel.entities import AgentType, Entity, Resource, ResourceType, RightsClaim
from authgate.kernel.registry import OwnershipRegistry
from authgate.kernel.verifier import Action, FreedomVerifier
from authgate.kernel.audit import AuditLog
registry = OwnershipRegistry()
human = Entity("alice", AgentType.HUMAN)
bot = Entity("analyst-bot", AgentType.MACHINE)
data = Resource("sales-data", ResourceType.DATASET, scope="/data/sales/")
registry.register_machine(bot, human)
registry.add_claim(RightsClaim(bot, data, can_read=True))
frozen = registry.freeze()
audit = AuditLog(path="/var/log/authgate.jsonl")
verifier = FreedomVerifier(frozen, audit_log=audit)
result = verifier.verify(Action("read-sales", actor=bot, resources_read=[data]))
print(result.summary())
assert audit.verify_chain()pip install -e .
authgate-cli verify --registry registry.json --action action.json --audit log.jsonl
authgate-cli audit verify /var/log/authgate.jsonlcargo build --features sandboxSandboxedExecutor wraps CallGate so permitted actions run with host imports limited to the rights bitmask. On Linux, pair with SeccompExecutor / SeccompCallGate for subprocess syscall confinement using the same rights mapping (authgate-kernel/src/seccomp.rs).
# Rust TCB
cd authgate-kernel && cargo test --lib
# Kani (selected harnesses)
cargo kani --harness prop_attenuation_two_node
cargo kani --harness prop_epoch_check
cargo kani --harness proof_forged_revocation_ignored
# Lean 4
cd formal/lean4 && lake build
# Python
pip install -e ".[dev]"
pytest
# Attack harness
python attack_harness/wire_attacks.py
python attack_harness/differential_tests.py
python attack_harness/mutation_attacks.pyEnforced on every verify() / CallGate::execute, in order:
| # | Name | Claim |
|---|---|---|
| I1 | CanonicalBinding | binding_hash == SHA-256(other fields) |
| I2 | IdentityBinding | capability subject matches actor |
| I3 | ExpiryGate | capability not expired |
| I4 | EpochSafety | leaf epoch ≥ min_epoch |
| I5 | ResourceBinding | capability resource matches action |
| I6 | Attenuation | child rights ⊆ parent rights at every hop |
| I7 | ChainEpoch | intermediate nodes also satisfy epoch |
| I8 | ChainComplete | every delegated cap in a Permit has a valid parent in the bundle |
| I9 | RevocationSafety | only root-signed revocations affect decisions |
authgate-kernel/ Rust kernel; TCB under src/tcb/; seccomp + session_clock helpers
formal/ TLA+, Kani, Lean 4, coverage & incompleteness notes
.github/workflows/ CI, formal.yml, seccomp.yml, sandbox.yml
attack_harness/ Wire / differential / mutation probes
src/authgate/ Python compatibility runtime + adapters (not TCB)
spec/ JSON Schema wire contract
examples/ Integrations (incl. Kubernetes sidecar)
docs/figures/ Architecture diagrams
INDUSTRY_READINESS.md Maturity tiers T1–T4 (assurance → production)
KEY_MANAGEMENT.md Vault / KMS / Key Vault integration guide
DISASTER_RECOVERY.md Root-key compromise & audit recovery runbooks
MIGRATION.md Registry/schema migration guide
All items from the original gap audit are closed or explicitly scoped. None remain open.
| Item | Resolution |
|---|---|
| WASM sandbox | Closed — Linux CI (.github/workflows/sandbox.yml); Windows local dev optional (SDK in DEPLOYMENT.md) |
| OS-level confinement (seccomp-bpf) | Closed — Linux CI adversarial test + rights-derived allowlist (.github/workflows/seccomp.yml); Windows/macOS: subprocess isolation only |
| TLC / Java tooling | Closed — CI-verified (.github/workflows/formal.yml); log in formal/tlc_run.log |
| CLI packaging | Closed — authgate-cli entry point + fresh-venv CI smoke; PyPI publish is release ops, not a gate gap |
| Refinement proof TLA+ → Rust | Out of scope — limitation L7, not an engineering gap |
| Distributed consensus in Rust TCB | Non-goal — NON_GOALS.md |
Infra-ready bar: this table must stay empty of open rows; see INFRA.md.
The intended long-term enforcement chain:
Agent → CallGate → capability-bound WASM (or OS sandbox) → restricted IO
| # | Limitation |
|---|---|
| L1 | Semantic content / natural-language intent is not gated |
| L2 | A malicious trust root is out of scope |
| L3 | Side channels not addressed |
| L4 | Python runtime is not formally verified |
| L5 | Heuristic extensions (IFC helpers, scorers) are not TCB |
| L6 | Clock is caller-supplied — use SessionClock / monotonic sourcing; backward jumps rejected within a session (see TCB_DISCIPLINE.md) |
| L7 | No implementation-level refinement proof from TLA+ to Rust |
Before changing anything under the TCB (authgate-kernel/src/tcb/):
Can this feature live entirely outside the TCB?
If yes, keep it out. TCB changes need an invariant justification, proof or model-check evidence where applicable, and regression coverage. See CONTRIBUTING.md and BRANCHES.md.
Source-available under the PolyForm Noncommercial License 1.0.0 — see also NOTICE.
| Use | Status |
|---|---|
| Evaluation / research / education | Allowed |
| Internal non-commercial testing | Allowed |
| Redistribution (non-commercial, with attribution) | Allowed |
| Production / commercial / SaaS / resale | Requires a commercial license |
| Patent rights | Reserved |
For production or commercial use, contact Ali Pourrahim — Alipourrahim.ap@gmail.com.