provable-action-adjudicator

name	provable-action-adjudicator
version	0.1.0
description	A runtime reference monitor that intercepts every proposed agent action, evaluates it against a policy DAG compiled from natural-language axioms, and returns a verified permit or deny verdict before execution proceeds. Policy axioms are authored in natural language, auto-formalized offline into Datalog (for relational/provenance policies) or Lean 4 decidable-arithmetic proofs (for numeric constraints), then evaluated at sub-millisecond to microsecond latency via aspect-woven join points at tool-call boundaries. The adjudicator is the provable containment layer for multi-agent systems: complete mediation, isolation, and formal correctness are the three non-negotiable properties.
author	soma-windags-graft
tags	["formal-verification","policy-enforcement","reference-monitor","lean4","datalog","active-inference","agent-safety","containment"]
pairs-with	[]
license	Apache-2.0
allowed-tools	Read,Write,Edit,Glob,Grep
metadata	{"provenance":{"kind":"imported","source":"workgroup-ai / windags skill library (rehomed 2026-07-04)"}}

Provable Action Adjudicator

When to Use

• An agent (or agent swarm) will invoke tools, write files, call APIs, or modify shared state, and you need a machine-checkable guarantee — not a heuristic filter — that those actions satisfy a stated policy before they execute.
• You are building a containment story for a multi-agent system: the orchestrator assigns tasks, but no individual agent should be trusted to self-police; a tamper-resistant interceptor must own the verdict.
• Natural-language policy documents (data-handling requirements, access controls, deontic obligations like "must log every PII read") need to be compiled into checkable axioms that survive iteration of the policy text without manual re-coding of enforcement logic.

NOT for:

• Post-hoc auditing or logging where actions have already executed — this skill is strictly preventive (and optionally corrective for soft constraints).
• Policies that require full LTL model checking over an unbounded state space at runtime — that is PSPACE-complete; offline model checking is the right tool.
• Replacing prompt-level safety instructions or RLHF alignment — the adjudicator operates on structured action objects at the tool-call boundary, not on token streams.

Core Concepts

Reference monitor (RM): The Anderson (1972) abstraction: a tamper-resistant interceptor that is (1) always invoked before every security-relevant action, (2) isolated from the agents it monitors, and (3) verifiable — its policy evaluation logic must be auditable. In the agentic context, "always invoked" means aspect-oriented join points woven at the tool-call boundary of the agent framework (LangChain, AutoGen, or a custom harness). The RM suspends the action, queries the policy engine, then resumes or aborts.

Policy DAG: A directed acyclic graph of policy axioms where edges encode logical entailment or dependency. Each node is a rule in Datalog-with-stratified- negation (Soufflé dialect). The DAG structure enables static analysis at compilation time: contradiction detection (a rule that both permits and denies the same action type), redundancy elimination, and subsumption checking (rule A already covers rule B). The DAG is the compiled artifact; natural language is the source.

Autoformalization pipeline: The offline process that translates natural- language policy statements into Datalog rules or Lean 4 theorems. An LLM drafts the formal representation; a static analyzer checks coverage (does the formal rule entail every case the NL sentence intends?) and flags edge cases for human review. This is research-grade for general NL but production-viable for constrained policy domains (access control, arithmetic thresholds). The compilation is expensive; the runtime evaluation of the compiled rules is cheap.

Proof generation vs. proof checking: For Lean 4 / decidable-arithmetic policies (e.g. "amount < 10000 AND recipient in approved_set"), the Lean kernel checks a pre-compiled proof in ~5µs (benchmarked on AWS Cedar). Proof via tactic search takes seconds to minutes and must happen offline during policy compilation. This separation is the architectural key to µs-latency formal verification: never generate proofs at runtime.