PerceptraAI Research

DARM Core is the research layer beneath the Guard.

The Guard page shows a runtime boundary. This page points to the formal research record: DARM Core v1.0, a machine-checked calculus for boundary-indexed assurance transfer.

Open Zenodo Record Formal Repository Guard Evidence Page

The paper

A formal account of when an assurance claim may move.

DARM Core separates assurance generation from assurance transfer. A theorem, contract, test, certificate, or assurance case may establish a source claim, but the target claim still needs a represented delta, boundary coverage, and discharge.

Problem

Unsupported expansion

A proof about one scope, authority, evidence source, enforcement locus, or representation is reused as if it covered a wider system.

Object

Assurance transfer

DARM asks what changed between source and target, which dependencies were introduced, and whether the target boundary covers them.

Result

Conservation rule

When source assurance and transfer admissibility hold, the target assurance claim becomes justified inside the model.

Calculus

SourceAssured plus admissible transfer yields TargetAssured.

The point is not that every true target claim must pass through DARM. The point is narrower and stronger: if a claim is being transported, DARM forces the introduced obligations into the open.

SourceAssured
  ∧ represented_delta(source, target)
  ∧ boundary_coverage(target, dependencies)
  ∧ discharge(target, dependencies)
  ⇒ TargetAssured

The Zenodo paper states this as an assurance-conservation discipline, supported by positive theorems, countermodels, localization results, and correspondence experiments.

What changes

The paper names the failure modes instead of smoothing them over.

Source claim

A local argument is valid.

A proof, test, contract, assurance case, or certification supports a bounded claim.

Transfer delta

The target introduces something new.

Scope, authority, locus, evidence, representation, composition, or relational structure changes.

Target claim

The new obligation must be discharged.

Without discharge, the source can remain true while the target claim is unsupported.

Research evidence

Formal corpus, archived paper, direct inspection paths.

This page points readers to the formal side of PerceptraAI's DARM work. The Guard page remains the runtime evidence page.

250

Lean modules

DARM Monitor local corpus snapshot used across the evidence site.

1,629

Theorems and lemmas

Declarations indexed in the formal repository materials.

Paper pages

DARM Core v1.0 PDF confirmed from uploaded metadata.

Declared axioms

For the reported corpus snapshot; trusted bases are still named separately.

Research object	Where to inspect	Boundary note
DARM Core v1.0 paper	Zenodo record 23214596	Archived research record, not a claim that every runtime implementation is proved.
Formal repository	Goblohan/darm-monitor	Lean model and proof corpus. Deployment behavior requires separate bridging evidence.
Guard/runtime repository	Goblohan/Darm-Guard	Runtime boundary and test evidence live here; they are not the same artifact as DARM Core.
Evidence page	PerceptraAI DARM Evidence	Use this for Guard claims, workflow status, closure experiment, and implementation limits.

Research position

DARM is not claiming to replace formal methods. It is locating the boundary between claims.

The paper's narrow novelty claim is that assurance transfer itself becomes a first-class, backend-independent, boundary-indexed object.

Reference monitorsThey mediate access. DARM asks what claim survives when the mediation boundary, evidence, authority, or representation changes.

Assurance casesThey already emphasize claims, evidence, and assumptions. DARM formalizes a transfer discipline that can reject unsupported expansion.

Contracts and runtime enforcementThey can generate source assurance. DARM then asks what extra target dependencies were introduced.

Verified systemsThey can prove implementation artifacts. DARM does not turn those proofs into broader claims without explicit adequacy and realization bridges.

Limits

The research page must stay honest.

Not global agent safety

The theory does not prove alignment, truthfulness, confidentiality, physical-world safety, or harm absence.

Not automatic implementation proof

A Lean theorem about a model does not by itself prove a Python service, OS, filesystem, compiler, or hosted deployment.

Not semantic adequacy for free

The chosen boundary must observe the distinctions the claim depends on. If it cannot observe them, DARM should not pretend it can enforce them.

Research links