Capability Safety as Datalog: A Foundational Equivalence
This foundational equivalence enables the transfer of algorithmic results to capability safety, potentially impacting security and AI safety domains.
The paper proves that capability safety can be exactly represented as propositional Datalog evaluation, addressing limitations in the existing capability hypergraph framework such as lack of efficient incremental maintenance and decision procedures for audit surface containment.
We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results unavailable in the native formulation. This addresses two structural limitations of the capability hypergraph framework of Spera [2026]: the absence of efficient incremental maintenance, and the absence of a decision procedure for audit surface containment. The equivalence is tight: capability hypergraphs correspond to exactly this fragment, no more.