Boundary-indexed assurance for agentic systems

DARM makes authority explicit before software acts.

DARM is PerceptraAI Lab's research line for claims that survive translation: model to implementation, representation to representation, theorem to running gate.

Open Research Page Open DARM Guard Open DARM Monitor Inspect Evidence

Runtime Trust Boundary

Make Python a requester, then test what it can still do.

The closure experiment moves authority and the governed workspace behind a protected publication service. A hostile Python requester may send arbitrary messages, but it cannot issue authority, alter signed content, replay an intent, or choose a stale predecessor version.

Requester

Proposal only

No workspace path, authority private key, policy object, or direct effect API. It receives a receipt and read-only status.

Protected service

Exact publication

Verifies a principal-signed intent, exact content digest, expected version, and one-time consumption before an atomic publication step.

Current experiment

12 HTTP + 4 transaction checks

Exact content, forged intent, replay, stale version, malformed request, receipt rollback, reopen survival, authority mismatch, and concurrent replay.

Bounded target

hostile_requester_behavior
  -> committed publication
  -> signed object + exact bytes + expected predecessor version

Current status: executable reference model. The service implementation, Python runtime, cryptography library, filesystem, crash recovery on every platform, OS isolation, and principal policy decision remain explicit trust or deployment obligations.

Read the closure experiment

What DARM Is

A discipline for warranted transfer.

DARM studies when an assurance claim may be transported across a boundary. The answer is not "because the systems are similar." The answer is a transfer warrant: what changed, what is preserved, and which obligation makes the target claim legitimate.

Boundary-indexed

Claims are indexed to the boundary they rely on, so a local guarantee is not silently reused as a broader system claim.

Representation-aware

Adequacy is property-specific. DARM asks whether the representation preserves what this claim actually needs.

Evidence-bearing

Every public assurance claim should name whether support is proved, constructed, tested, assumed, or not yet established.

DARM Guard

A working authorization broker for governed effects.

DARM Guard places an execution boundary between an agent and its tools. The agent can propose. The broker holds the tools, asks the compiled DARM kernel, executes only the admitted invocation, and leaves signed evidence.

Pinned repository counts

Claims

Effect sites

Mutations

Gate steps

Snapshot: DARM Guard commit 4bcab18. Package/kernel row in repository README: 0.28.0 / kernel-v0.4.0.

Runtime boundary

01 / Canonicalization

One invocation, from proposal to effect.

The broker assigns provenance from a principal-controlled registry and freezes the invocation before asking the kernel. The admitted invocation is the one sent to execution.

Boundary: Python-to-model correspondence is tested, not proved. Complete mediation depends on deployment.

broker.py / Broker.decide

Source path: broker.py and kernel.py. Enable JavaScript to inspect individual nodes.

Evidence Ledger

Marketing language that can survive review.

The page below separates formal corpus evidence, runtime evidence, repository workflow evidence, and limitations. It is built from the current local clones and the claim graph pinned to DARM Monitor commit caebc7c.

250

Lean modules

158 GRBS modules and 92 DarmMonitor modules.

1,629

Theorems and lemmas

Corpus count from Monitor stats.

47,524

Lines of Lean

All corpus modules counted.

0 / 0

Sorry / axioms

Zero files with sorry, zero declared axioms.

Public claim	Evidence handle	Status
Every Guard claim cites its supporting theorem or marks itself unmodelled.	assurance/claims.json, checked by check_assurance.py	31/31 fully cited
Formal claims also carry gated runtime evidence.	Claim graph pinned to darm-monitor caebc7c	27/27 formal claims
The runtime effect surface is closed under the repository inventory.	effect_sites.json, checked by check_effect_sites.py	53/53 classified, 0 open
The Monitor paper does not cite missing theorem names.	paper/check_citations.py	83/83 citations exist
Bridge type is explicit for model-to-code movement.	check_bridges.py	1 construction, 1 proved, 29 tested, 0 assumed
The reference deployment can require exact, single-use intent consumption in addition to the kernel verdict.	DARM Guard 8e4a045, tests/deployment_intents.py, and deployment-intents.md	14 deployment checks + 3 real-kernel intent tests
The confined agent cannot create files beside the broker socket in the Compose deployment.	Mediation workflow #160 on hardening/agent-socket-readonly	HTTP path absent, network absent, root filesystem read-only, socket directory read-only

Workflow Evidence

What runs, and why it matters.

Selected GitHub Actions runs, separate from the pinned repository-count snapshot above. A passing run reports that workflow's outcome, not an end-to-end proof.

Guard gate

Adversarial probes

Not checked

main / push

No live result loaded.

View workflow runs

Runs the demo fixture, evidence attacks, broker attacks, runtime correspondence samples, assurance graph, effect inventory, mutation gate, and workflow validation.

Workflow · Actions

Mediation

Reference deployment

Not checked

hardening branch / manual dispatch

No live result loaded.

Inspect run #160

Tests the containerized deployment where the agent has no workspace, no network, only a read-only broker socket directory, and exact single-use intents for governed effects.

Workflow · Compose file · Intent tests

Formal CI

Lean action and corpus elaboration

Not checked

main / push

No live result loaded.

View workflow runs

Checks placeholder absence, audits axiom traces, elaborates the complete corpus, builds native code, and runs runtime differential tests.

Workflow · Actions

Theory Map

From representation adequacy to runtime identity.

The formal work is not a single mega-claim. It is a set of bounded results about transfer, authority, representation, evidence, and implementation change.

R3e boundary stressShows how the stronger novelty claim fails under PhysicalAG, refining DARM into an explicit assurance-transfer discipline.

R4 dimensionsScope, authority, locus, evidence, and composition are isolated by attacks, then stated as transfer obligations.

K5 to K7Theorems about the shipped server path: admitted replies, canonical invocation, and reply nonce binding.

B and E seriesBroker models, intents, evidence before effect, execution identity, remote effects, attested channels, and assurance under change.

Read the DARM Core research page

Inspect the Lean 4 signatures

Research-branch excerpts at 8ff950f (research/e37-heterogeneous-warrant). These are not part of the main-branch corpus snapshot or its live CI badge above. Proof bodies and definitions are linked in source.

E35 Representation adequacy Lean signature

An adequate observation preserves the chosen property from a reviewed value to an observationally equal candidate.

theorem observed_preserved {V O : Type} {observe : V → O} {P : V → Prop}
    (hA : AdequateFor observe P) {r v : V} (hR : P r)
    (hG : ObservedGate observe r v) : P v

Namespace: DARM.E35. Requires property-specific adequacy, a reviewed property, and observation equality. It does not formalize Python or prove the implementation bridge.

Declaration, definitions, and proof

E36 Finite transition chains Lean signature

Initial adequacy survives a finite chain when every transition discharges its local preservation obligation.

theorem chain_preserves {V O : Type} (P : V → Prop)
    (observe : V → O) :
    ∀ steps, DARM.E35.AdequateFor observe P →
      ChainObligations P observe steps →
      DARM.E35.AdequateFor (chainObservation observe steps) P

Namespace: DARM.E36. One common observation type and one chosen property. This is not an executable search for arbitrary semantic equivalence.

Declaration, obligations, and proof

E37 Heterogeneous warranted transfer Lean signature

Inside a valid boundary, a target claim holds exactly when it has inherited or local warrant.

theorem target_claim_iff_entitled
    {S T : Type}
    {b : Boundary S T}
    (hValid : Valid b)
    {t : T}
    (hTarget : b.target t) :
    b.targetClaim t ↔ Entitled b t

Namespace: DARM.E37. Valid requires transfer soundness, local-warrant soundness, and no unsupported introduction. Internal validity alone does not establish an external-world claim.

Declaration, boundary conditions, and proof

Try The Runtime

Start with the demo, then inspect the evidence.

The runtime path is intentionally concrete. Install, install the pinned kernel, run the demo, then inspect the audit trail and evidence report.

Package

pip install darm-guard
darm-guard-install-kernel
darm-guard demo

Container

docker run --rm ghcr.io/goblohan/darm-guard darm-guard demo

Repository gates / from a Guard clone

./tests/setup_demo.sh
python3 scripts/ci_local.py

Prior Art

DARM is narrow by design.

The site should not pretend reference monitors, assurance cases, taint tracking, runtime enforcement, verified kernels, or agent security benchmarks do not exist. The claim is narrower: DARM makes assurance scope, authority, enforcement locus, and evidentiary basis explicit and machine-checkable.

Area	Representative works	DARM position
Reference monitors and complete mediation	Anderson, Saltzer and Schroeder	DARM Guard is a reference monitor for agent tool use, with complete mediation stated as an assumption rather than magically proved.
Tamper-evident logs	Kelsey and Schneier, Crosby and Wallach	DARM uses audit evidence to bind freshness and effect identity, not only to detect log tampering.
Verified systems	seL4, translation validation, HACL*	DARM does not verify the whole Python runtime. It names which bridge is construction, proved, tested, or assumed.
Agent defenses	CaMeL, FIDES, Progent, AgentSpec, prompt-injection design patterns, AgentDojo	DARM acts at execution and effect, then checks the state and evidence that remain after the tool call.
Runtime enforcement and information flow	Schneider enforceable policies, information-flow control for agents	DARM asks what the boundary observes and what claims can be complete relative to that observation.

Source map: paper/related.md and references.bib.

Limits

What the site must not claim.

This is the difference between a serious research page and a sales page wearing theorem makeup.

Not a sandbox

DARM Guard assumes complete mediation. The agent must reach governed files and governed network effects only through the broker.

Closure is bounded

The requester cannot widen one publication in the reference model. The protected service, deployment isolation, storage behavior, and Python implementation still need separate evidence.

Not global safety

DARM does not claim physical-world safety, content truth, harm detection, confidentiality, or universal semantic adequacy.

Full source: DARM Guard limitations and DARM Monitor limitations.

Repositories And Handles

Inspect the work directly.

The public page should send serious readers to the exact places where claims can be checked.

Runtime repository

DARM makes authority explicit before software acts.

Make Python a requester, then test what it can still do.

Proposal only

Exact publication

12 HTTP + 4 transaction checks

A discipline for warranted transfer.

Boundary-indexed

Representation-aware

Evidence-bearing

A working authorization broker for governed effects.

One invocation, from proposal to effect.

Marketing language that can survive review.

What runs, and why it matters.

Adversarial probes

Reference deployment

Lean action and corpus elaboration

From representation adequacy to runtime identity.

Start with the demo, then inspect the evidence.

DARM is narrow by design.

What the site must not claim.

Not a sandbox

Closure is bounded

Not global safety

Inspect the work directly.

DARM Guard

DARM Monitor

DARM Core

Zenodo record

PyPI darm-guard

Module Index

Python requester closure