DARM Guard

See what your agent is doing. Then govern it.

An agent tool-authorization guard, grounded in a machine-checked Lean 4 theory of assurance transfer.

PerceptraAI Lab

Install

pip install darm-guard

Quick Start

from darm_guard import DARMGuard, Policy, Credential

guard = DARMGuard(
    policy=Policy(authorized_tools=frozenset(["file_read", "web_search"])),
    credential=Credential(tools=frozenset(["file_read"])),
)

guard.check({"file_read"})   # admitted, within credential
guard.check({"code_exec"})   # admitted in OBSERVE mode, but reported

Kernel-backed guard (v0.3, recommended)

KernelGuard checks the tool, its arguments, and where each argument came from. Every allow/deny decision is computed by the DARM decision kernel: a Lean 4 function with machine-checked properties (darm-monitor K1DecisionKernel), compiled to a native binary (K2DecisionServer). The Python side only formats requests.

from darm_guard import KernelGuard, KernelPolicy, ToolRule, ArgRule

policy = KernelPolicy(tools=(
    ToolRule("file_read", (ArgRule("path", allowed_prefixes=("/workspace/",)),)),
))
guard = KernelGuard(policy, tools={"file_read"},
                    default_provenance="untrusted",
                    kernel_path="/path/to/darmkernel")

guard.check("file_read", {"path": "/workspace/notes.txt"},
            provenance={"path": "authoritative"})         # admitted
guard.check("file_read", {"path": "/etc/passwd"},
            provenance={"path": "authoritative"})         # rejected: semantic
guard.check("file_read", {"path": "/workspace/notes.txt"})  # rejected: provenance

Proved about the kernel's decision function: an admitted invocation passed all five checks, and an expired credential, a tool outside the credential, or any untrusted argument value can never be admitted.

Install the kernel. After pip install darm-guard, run darm-guard-install-kernel. It downloads the kernel binary that darm-monitor's CI built from tag kernel-v0.1.0 and installs it only if its SHA-256 matches the value pinned in this package. Linux x86_64 only; elsewhere, build it with lake build darmkernel and set DARM_KERNEL_PATH. Kernels are never downloaded during an authorization check.

Limits. Not proved: this Python module, JSON encoding, argument-to-string conversion, expiry computation, the kernel's JSON parser and I/O loop, and the Lean compiler. The guard fails closed if the kernel is missing, crashes, or times out. Provenance labels come from the caller; the guard does not infer lineage.

DARM Verify (v0.4)

Check any authorization gate against the DARM kernel. Wrap the gate in an adapter, a function from a DARM request to a Verdict. Verify runs seeded scenarios through both the gate and the kernel and reports every disagreement:

• false admit: the gate allows what the kernel rejects, labeled with the kernel's reason (T, O, A, S, or P)

• false reject: the gate blocks what the kernel admits

  darm-verify --adapter darmguard-v0.1 --n 1000 --json report.json

Worked example: DARM Guard's own v0.1, 1,000 scenarios, seed 20260922:

No false rejects. Every false admit matches a mechanism stated in darm-monitor's formalization of v0.1 (IC1RuntimeSemantics, R22), checked case by case against the saved report.

Writing an adapter for your own gate:

from darm_guard.verify import verify, Verdict

def my_gate(req):     # req has "policy", "credential", "invocation"
    ...               # translate req into your gate's terms and ask it
    return Verdict(admitted, reason)

print(verify("my-gate", my_gate, n=1000).summary())

Scope. Divergences are measured against the kernel's semantics and against your adapter's translation of each scenario, so a divergence can mean a gap in the gate or a limit of the translation. The JSON report includes every scenario so a person can tell which. Scenarios are generated from a small vocabulary: they test decision logic, not real workloads. Verify requires the kernel (darm-guard-install-kernel) and stops if the kernel errors, rather than reporting without a referee.

Three Modes

OBSERVE (default) -- logs and classifies every call. Never blocks. Prints a warning saying so.

GOVERN -- returns a rejection with a typed diagnosis. Your code must honour it.

ENFORCE -- as GOVERN, plus an append-only JSON-lines audit file.

from darm_guard import Mode
guard = DARMGuard(policy=p, credential=c, mode=Mode.GOVERN)
result = guard.check({"code_exec"})
# result.admitted == False
# O-failure: code_exec -- not in observation model

Claim strata

Each layer's claim is weaker than the one above it, and none inherits another's.

What is and is not guaranteed

The v0.1 DARMGuard API operates at the tool-name level, and the notes below apply to it. For argument-level, kernel-computed decisions, use KernelGuard (above). It is grounded in a machine-checked Lean theory, but the Python runtime itself is not formally verified.

Guaranteed by the runtime:

• Credentials and policies are immutable once constructed.
• The delta (requested tools not in the credential) is computed exactly.
• Decisions are deterministic: the same inputs give the same result.
• Within one process, every check is appended to the session audit log.

Proved in Lean about this runtime (darm-monitor):

• The v0.1.0 decision rule is formalized exactly and proved equivalent to a single inclusion condition (IC1RuntimeSemantics).
• Because v0.1.x observes only tool names, no authorizer built on its observations can separate a safe call from a forbidden call to the same tool (R22RuntimeImplementationCorrespondence).
• A runtime that also observes arguments recovers that distinction (R22). This is the specification for v0.2.

Not guaranteed -- assumed:

• Complete mediation: calls that bypass the guard are invisible to it.
• Enforcement: in GOVERN mode the guard returns a decision; it cannot stop code that ignores it.
• Argument-level or effect-level safety: file_read on any path is treated the same.
• Authorization of credential expansion: update_credential is not access-controlled.
• Freshness at execution time: expiry is checked when check() runs, not when the tool runs.
• Session state across processes or restarts.
• The D (domain) and S (semantic) conditions: classified in the theory, not enforced at runtime.

ODATS Diagnosis

Each condition is proved independently necessary in the Lean theory: removing any one admits a countermodel.

Session Scope Tracking

Tracks cumulative scope across a session, within one process.

guard.check({"file_read"})
guard.check({"web_search"})
print(guard.scope())   # cumulative scope and drift

Temporal Freshness

from datetime import datetime, timedelta
cred = Credential(tools=frozenset(["file_read"]),
                  issued_at=datetime(2026, 9, 1), ttl=timedelta(hours=4))

LangChain Integration

from darm_guard.integrations import guard_tools
guarded = guard_tools(agent.tools, guard=my_guard)

Formal Backing

The conditions behind each check are proved in darm-monitor. See FORMAL_BACKING.md for the theorem map. 1,100+ theorems, zero sorry, CI-audited for sorryAx.

Roadmap

• v0.3 -- KernelGuard: invocation-level, provenance-aware, decisions computed by the Lean kernel.
• v0.4 (this release) -- DARM Verify; proved kernel correspondence to E17, E18, and R22 (K3); kernel-checked certification of the shipped binary.
• Next -- Verify adapters for third-party gates, published only with their maintainers' involvement; epistemic premise transfer (E24); an enforcement broker for one domain.
• Later -- credential-holding enforcement broker for one domain; gated credential expansion.

License

MIT

Olusanya Gbolahan V -- PerceptraAI Lab