PolicyStrata

Abstract

LLM data agents repeat policy obligations across model-visible capabilities, validators, query compilers, database controls, and result-release logic. Each component may pass its own tests while a mismatch between components exposes the wrong capability, produces unauthorized SQL, or releases a disallowed result.

We present PolicyStrata, a deterministic regression tester for this cross-layer policy drift. It checks each transition in execution order and emits a replayable witness for the first violated contract. Its v1 benchmark defines 22 mutation operators across three synthetic analytics domains. PolicyStrata detected all 1720 represented fault cases and emitted no witness for 80 clean controls. This result measures coverage of the implemented fault model, not recall on unknown production failures. A conventional specification-derived suite missed 141 cases, a layered point-control stack missed 159, and a spec-blind suite agreed with PolicyStrata on 39 of 42 cases.

Separate studies test the method beyond its generated fixtures. Across 75 real-SQL traces from four independently maintained open-source systems, the scan produced one content-level false positive and exposed five adapter gaps, which were fixed. Executing 20 upstream row-level-security policies in PostgreSQL passed 13 containment checks; weakening one predicate failed only the checks that covered it. A frozen MetricFlow revision reproduced 68 upstream-authored expected-SQL cases byte-for-byte. A maintainer-operated deployment study matched inspected source to the deployed revision and passed 33 read-only denial-boundary probes; three authenticated probes were unavailable. Private-source replay reproduced three historical fixes. These studies establish a reproducible fault-model result and a concrete retargeting path. They do not establish field recall or independently operated deployment effectiveness.

1 Introduction

An LLM data agent turns a request into a structured plan, an executable query, and a released answer. Policy enters this path more than once. A capability manifest tells the model what it may request. A grammar defines valid plans. A validator accepts or rejects a plan. A compiler turns the plan into SQL. Database policy constrains execution, and a release check decides what may leave the trusted boundary. We call these six components the policy pipeline. They use different representations and may be deployed on different schedules.

Each component may pass its own tests while a transition between components drops tenant identity, changes a metric definition, uses a stale alias, loses lineage, or releases a result under an obsolete rule. We call a mismatch between a canonical obligation and a policy-pipeline surface divergence. When an update creates the mismatch, we call it policy drift.

Worked example.

Suppose analyst Alice belongs to tenant $A$ and may request tenant-$A$ ticket aggregates, but not tenant-$B$ rows or raw customer email. The canonical policy is version 7. The validator also runs v7, while the compiler still runs v5 and uses legacy_tenant_id. Alice asks for “escalations by region.” The validator accepts the semantic plan Accepted semantic plan⟨escalated_tickets, [region], last_month, 100⟩$$\langle\texttt{escalated\_tickets},[\texttt{region}], \texttt{last\_month},100\rangle .$$ Compiling that accepted plan is a lowering: a translation from the typed plan into SQL. The stale compiler binds the tenant obligation to the wrong column. On a two-row database containing one distinguishing tenant-$B$ escalation, the emitted SQL reads both tenants. Database row-level security (RLS) may block the extra row, but that containment does not make the compiler correct.

PolicyStrata records the six deployed versions as a version vector, here Deployed version vectormanifest grammar validator compiler database release 7 7 7 5 7 7$$\begin{aligned} \vec{v}={}&(v_{\mathrm{manifest}},v_{\mathrm{grammar}},v_{\mathrm{validator}},\\ &v_{\mathrm{compiler}},v_{\mathrm{db}},v_{\mathrm{release}}) =(7,7,7,5,7,7). \end{aligned}$$ It evaluates the canonical plan and the lowered query, checks each transition in order, and reports the compiler as the first violated contract. The witness retains Alice, the plan, the version vector, the distinguishing rows, the SQL, the RLS outcome, and the release decision. This example separates three facts that a final-answer assertion would collapse: the compiler violated tenant preservation, RLS contained the violation, and no external disclosure occurred.

The right oracle is therefore not literal equality between layers. A manifest may intentionally expose less than a validator accepts, and RLS may intentionally be stricter than an application check. PolicyStrata assigns each surface a responsibility and checks only the obligations that surface accepts or emits.

Scope and evidence boundary.

PolicyStrata is a regression tester and scanner, not an authorization boundary. It assumes a human-reviewed canonical policy and trusted adapters that map implementation artifacts into the checking model. The v1 benchmark covers single-request, read-only analytics. Its deterministic generator and simulator share the same public operator taxonomy. The 1720/1720 result therefore measures internal fault-model coverage, not production recall. A maintainer-operated deployment study verifies source-to-deployment binding and selected live denial behavior. It reports only aggregate results, reads no customer rows, and lacks an authenticated synthetic principal. No study observes an independently operated deployment or estimates recall on unknown production incidents.

Claims and non-claims.

Contributions.

This paper contributes:

• a model of a data agent as six non-equivalent policy surfaces with explicit exposure, validation, lowering, containment, and release contracts;

• a deterministic generator and replay checker that produces first-transition witnesses, plus counterfactual repair checks for attribution and bounded replay reduction for witness size;

• DataPolicyDriftBench, with 22 named operators, explicit suite provenance, equivalent/invalid accounting, freeze manifests, two spec-derived comparators, and separate synthetic, spec-blind, public-fault, brownfield, and historical-revision evidence;

• a documented retargeting contract plus an aggregate, deployment-linked read-only study whose private operational identifiers are withheld.

2 Background and Related Work

Six research lines touch parts of the policy pipeline, but they answer different questions.

Access-control analysis and mutation testing.

Margrave computes semantic differences between two access-control policies and can explain requests whose decisions change [7]. XACML mutation work defines policy fault operators, test adequacy, and equivalent-mutant handling [18]. Cedar compares an authorization implementation with an independently specified model through formal and differential testing [5]. These methods can analyze a policy language more deeply than PolicyStrata and may prove or systematically test decision equivalence inside that language. They do not by themselves connect a model-visible metric alias, semantic plan, SQL lowering, runtime database role, and result-release decision. PolicyStrata borrows mutation adequacy and differential-oracle ideas, but makes the unit of analysis a heterogeneous transition in the policy pipeline.

Translation validation and property-preserving compilation.

PolicyStrata’s compiler contract is an instance of translation validation: rather than proving a compiler correct once, check each individual compilation against its input [21]. Secure-compilation work sharpens what such a check should preserve, distinguishing full abstraction from the weaker robust preservation of specific property classes across a compilation boundary [1]. Authorization-preserving lowering is deliberately the weaker, property-class form: we do not ask a compiler to preserve all observational equivalences, only the declared obligations of principal, tenant, purpose, policy version, lineage, and metric semantics. What PolicyStrata adds is neither a new preservation theorem nor a proof technique, but the observation that a data agent runs several such lowerings between representations that are separately versioned, so a preservation failure must be attributed to one transition rather than to the pipeline as a whole.

SQL checking and generated databases.

Distilled test-suite accuracy constructs databases that distinguish candidate SQL from a reference query [33]; VeriEQL and SpotIt+ reason about bounded query equivalence under supported SQL semantics and constraints [9], [27]. Such tools give stronger SQL-level semantic evidence than finite execution alone. They do not decide whether a query was exposed to the right principal, retained tenant identity and policy version, used authorized lineage, or crossed an allowed release boundary. Conversely, PolicyStrata does not prove general SQL equivalence: its database states are finite witnesses, and a supported SQL verifier could replace that one checker.

Database and agent enforcement.

Beacon checks consistency within DBMS access-control metadata and behavior [20], and row-level security is the containment mechanism our database contract observes [22]. Agent enforcement systems place deterministic policy or privilege controls around tool execution [19], [25]; Cordon adds a transactional boundary that stages irreversible effects until a composed execution flow validates [3]; C-Trace compiles a subset of GDPR into predicates over execution traces and rejects non-compliant actions at runtime [10]; Data Flow Control pushes tuple-level release policy into the DBMS through provenance-aware query rewriting [26]; and role-conditioned refusal work evaluates model-level compliance [11]. These systems can block behavior at runtime. PolicyStrata instead tests whether separately maintained enforcement surfaces still agree with their assigned contracts, and it reports an upstream compiler violation even when RLS safely contains it. The relationship is complementary in both directions: an enforcement layer is a surface PolicyStrata can observe, and PolicyStrata is a way to detect that such a layer has drifted from the specification it was deployed to enforce.

Agent conformance testing and drift.

The closest recent work shares our premise that agent safety degrades between components rather than inside one. Constraint drift argues that safety-critical constraints lose force as they pass through memory, delegation, communication, tool use, and audit, and that asserting a constraint once is not the same as maintaining it [15]. PolicyStrata is a narrow, executable instance of that position for a single-agent data pipeline: six named surfaces, declared obligations per transition, and a checker that reports where an obligation stopped holding. AgentRFC extracts normative clauses from agent protocol specifications into a typed IR, model-checks them, and replays counterexamples against live SDKs [32]; its extract-check-replay shape is close to ours, but its subject is protocol conformance between agents rather than policy obligations between representations inside one agent. TDAD treats prompts as compiled artifacts and applies hidden test splits and semantic mutation testing to agent specifications [23], which is the same adequacy argument we make for a cross-layer operator registry. AgentRaft detects data over-exposure by building a cross-tool call graph, tracking taint at runtime, and adjudicating with a model committee [16]; it covers tool-to-tool flows that PolicyStrata does not model, while PolicyStrata stays deterministic, needs no model at scoring time, and localizes to a versioned transition rather than to a flow.

Generation and task benchmarks.

Spider, BIRD, DAB, BEAVER, and DAComp measure SQL or data-task capability [2], [12], [14], [17], [31], while $\tau$-bench and ST-WebAgentBench measure whether agents follow domain rules and safety policies during interaction [13], [30]. PICARD and structured decoders reduce malformed outputs [6], [8], [24], [29]. Correct, rule-following, or grammar-valid output can still select the wrong tenant, implement the wrong business metric, or violate release policy once it is lowered to SQL. PolicyStrata therefore starts at typed semantic IR; stochastic natural-language-to-plan reachability is reported separately and is not part of its deterministic score. A recent security study of data agents supplies the independent fault vocabulary we test our registry against [28]; LASM supplies a second, structural taxonomy derived from 116 agent-security papers [4].

The table is a capability comparison, not an empirical ranking: these systems were not run as drop-in competitors because they accept different languages and prove or test different properties. A fair composition would use Margrave or Cedar as the authorization oracle, VeriEQL as the compiler-semantic checker, and database/runtime monitors as observed surfaces inside PolicyStrata’s transition harness. The novelty boundary is therefore narrow. PolicyStrata is not a new policy logic, SQL verifier, or reference monitor. It composes evidence across versioned, non-equivalent representations and assigns a failed obligation to the first transition responsible for preserving it.

3 Model and Guarantee Boundary

Let a data-agent pipeline have runtime objects:

$$X_0 \to X_1 \to X_2 \to X_3 \to X_4$$

The representations may correspond to a model-visible request, a typed semantic plan, a validated executable plan, a SQL query and execution context, and a released analytical result. The surfaces that handle those objects are related but not interchangeable:

The surface-specific contracts used by PolicyStrata are summarized in Table 1. The formal definitions appear in Appendix A.

A grammar is a language recognizer. A validator is a decision procedure. A compiler is a partial lowering function. RLS is an execution-time reference monitor. A manifest is a projection shown to the model. Treating these as one kind of object obscures the bugs we want to find.

At version $t$, the canonical policy separates authorization, semantic, and release specifications: $P^t=(P_{\mathsf{auth}}^t,P_{\mathsf{sem}}^t,P_{\mathsf{rel}}^t)$. The authorization specification defines who may perform operations over rows, columns, metrics, tenants, and purposes. The semantic specification defines the meanings of metrics, dimensions, aliases, grains, joins, filters, and time windows. The release specification defines whether a result and its lineage may leave a trusted boundary. These are intentionally separate: a correct RBAC decision cannot prove that “net revenue” used the right denominator, and a semantically correct aggregate may still be unsafe to disclose.

Exposure soundness.

A model-visible manifest or grammar is exposure-sound if every operation reachable through an exposed capability is authorized for the principal and context. This does not require every authorized capability to be exposed.

Declared completeness.

Over-restrictive behavior is a defect only inside the advertised support envelope. This avoids treating intentional underexposure, feature flags, stricter release suppression, or unsupported-but-authorized requests as bugs.

Authorization-preserving lowering.

Lowering must also preserve security-relevant context: principal, tenant, purpose, jurisdiction, policy version, release boundary, and time semantics cannot be silently dropped. This property catches compilers that accept a valid plan but emit SQL that reads the wrong tenant, expands a metric into forbidden columns, or uses stale identity keys.

Semantic translation validation.

PolicyStrata searches for admissible database states where the lowered query and the reference semantic plan produce different observations. The comparison must define bag versus set semantics, ordering, floating-point tolerance, NULL and three-valued logic, errors, timestamp and timezone behavior, and nondeterministic functions. Testing finitely many generated states finds distinguishing witnesses; it does not prove general SQL equivalence unless paired with a verifier such as bounded SQL-equivalence checking [9], [27]. Semantic equality is not sufficient for authorization: two queries can return the same visible result while one scans forbidden rows or columns. PolicyStrata therefore checks both denotational behavior and dependency or lineage conformance.

Release conformance.

For v1, release is stateless and single-query: a result and its lineage may leave a boundary only if the release policy permits that pair for the principal and context. A release boundary may be the human user, the LLM context, an external model provider, a log, a cache, or another tool. Raw unauthorized rows entering an untrusted model context can be a disclosure even if the final user-facing answer is suppressed.

Witness classes.

PolicyStrata reports over-permissive exposure, over-restrictive rejection, lowering violation, semantic drift, and unsafe release. The v1 mutation registry instantiates four of these classes; over-restrictive behavior is supported by the detector but absent from the 22-operator generated benchmark.

Drift witness.

A drift witness records the principal, request, semantic IR, version vector, lowered SQL, observed database result, release decision, surface responsibilities, contract decisions, first violated transition, and explanatory reasons. The current emitted witness does not reduce arbitrary source code, policy clauses, database rows, or SQL structure. Its bounded reducer only removes semantic-IR dimensions and filters or resets a non-default limit, replaying after each edit to preserve witness class, localized surface, containment layer, release decision, and relevant semantic or database evidence.

Divergence, drift, and version skew.

A static mismatch present from initial deployment is policy divergence. Update-induced drift exists when the pipeline satisfied expected contracts before an update but fails afterward. A version vector is simply the ordered version identifier for each of the six surfaces. It lets a test reproduce partial rollouts and stale caches instead of recording only one application version. PolicyStrata can detect divergence and skew only when the canonical specification or another independent oracle disagrees with the implementation. It cannot detect a common-mode error where every surface faithfully implements a bad canonical policy.

Contract-relative soundness.

For an emitted trace $T$, let $\mathsf{Witness}(T)$ mean the detector reports a non-clean class and let $\mathsf{Violation}(T)$ mean at least one modeled surface contract fails or an unauthorized result is released. The checked invariant is $$\mathsf{Witness}(T)\Rightarrow\mathsf{Violation}(T).$$ The implementation tests this property with 400 property-generated examples and an exhaustive sweep of applicable operator/domain combinations over 25 seeds. No counterexample was found. This is evidence that the detector does not invent a witness relative to its own contracts and simulator. It is not a mechanized proof, does not validate the canonical policy or adapters, and does not imply the converse for faults outside the 22 operators.

4 Checking Procedure

PolicyStrata separates the reference model, observed surfaces, and labels. The canonical policy is YAML validated into principals, roles, metrics, dimensions, aliases, grains, cost and row bounds, and tenant scopes. A second YAML document declares the six surface versions, each surface’s responsibility, and the obligations passed between surfaces. A semantic query is a typed tuple of metric, dimensions, filters, time range, grain, and limit. Static suites or imported JSONL traces supply the remaining test inputs.

Specification language.

The language is deliberately a typed data schema rather than a new policy calculus. Authored policy and surface files reject unknown fields. A shortened, valid fragment is:

roles:
  analyst:
    allowed_metrics: [ticket_count]
    allowed_dimensions: [region]
    max_rows: 1000
contracts:
  compiler:
    mode: sql_lowering
    accepts_obligations: [tenant_scope]
    emits_obligations: [sql_semantics]

Metric declarations bind a semantic name to an expression, source table, columns, aliases, roles, grain, and estimated cost. Principal declarations bind a role and tenant identifiers. The surface file does not encode executable enforcement; it declares what an adapter must observe and what the checker will hold that transition responsible for. Imported JSONL then supplies an observed principal, SQL, optional semantic IR, tenant bindings, release outcome, source, and regression label. Missing semantic IR disables semantic-oracle checks for that trace rather than synthesizing a meaning.

Reference and implementation paths.

The reference interpreter decides whether the semantic query is authorized and computes the intended metric and release conditions. The implementation path simulates or imports manifest exposure, grammar membership, validator output, compiled SQL, database effects, and release output. The reference interpreter does not call the SQL compiler. This separation prevents compiler behavior from defining its own oracle, but a shared error in the policy file or adapters remains possible.

Cross-layer conformance analysis.

For each case, the checker performs the following steps:

1. Load principal $p$, query $q$, database state $D$, canonical policy version $t$, and surface-version vector $\vec{v}$.

2. Evaluate $q$ with the reference authorization and semantic interpreters.

3. Replay the six surfaces in execution order. Each adapter emits its decision and the obligations it passes downstream.

4. Evaluate only the declared contract at each surface. For example, the compiler check compares tenant binding, metric expression, grain, time semantics, cost, and lineage; it does not require its representation to equal the validator’s.

5. Select the first failing contract in the fixed order manifest, grammar, validator, compiler, database, release. Later enforcement can be recorded as containment without erasing the earlier violation.

6. Replay bounded reductions and emit the smallest witness reached under the reducer’s move set.

The selection rule is deterministic. If $F_i(T)$ is the Boolean contract result for surface $i$, localization returns $\min\{i\mid \neg F_i(T)\}$ in pipeline order. Only if no declared contract fails does it compare the final release with the canonical decision. This distinction is why a compiler failure remains attributed to the compiler when the database later contains it.

A mutant is killed when this procedure emits a non-clean witness. It survives when no modeled contract fails. A mutant is equivalent when an injected change produces no policy-observable difference for the chosen principal, query, and state; it is invalid (or stillborn) when it cannot form a valid test case. Clean controls contain no injected drift and become false positives if a witness is emitted.

Attribution versus root cause.

The reported location is the first observed violated transition, not a source-code root cause. We test this attribution interventionally on compound cases. Repairing the attributed surface must move or eliminate the first violation (sufficiency), while repairing a later, non-attributed surface must leave the earlier attribution intact (necessity). A teeth test that forces a constant wrong attribution fails these checks. This is stronger than matching a fixture label, but it remains relative to the simulator and distinct-surface mutation model.

Witness reduction.

The reducer tries one edit at a time: remove a semantic-query dimension, remove a filter, or reset a non-default limit. It accepts an edit only after replay preserves the witness class, first failing surface, containment layer, release decision, the localized failed contract, and any semantic-difference or database-containment fact needed by the original witness. The search stops after 32 attempts or a fixed point. Standard support suites reach 1-minimality under this move set, with median semantic-IR reductions of roughly 2% for seeded cases and 6% for generated cases. One-minimal means no single remaining edit in this three-operation neighborhood preserves the witness; it does not mean globally shortest JSON, SQL, policy, or database state. Because generated inputs are already narrow, this is diagnostic compaction, not general delta debugging.

5 Retargeting PolicyStrata

PolicyStrata is a Python package and command-line tool. The deterministic paper path needs no LLM API key and runs with scripts/reproduce-final.sh. It writes materialized tasks, JSONL traces, summaries, witnesses, comparator results, ablations, and benchmark manifests. Optional PostgreSQL and ClickHouse services exercise database-policy fixtures but are not included in the 1720-case score.

What a new target must provide.

Retargeting is a specification and adapter task, not automatic source-code analysis. The minimum domain package contains:

1. a canonical policy mapping real principals or roles to allowed metrics, dimensions, time ranges, row and cost limits, and tenant scopes;

2. a surface contract naming the policy-pipeline versions and the obligations each available surface accepts and emits;

3. representative semantic queries or imported traces with principal identity, SQL or semantic IR, and release outcome;

4. adapters or configuration that connect real names, tenant columns, semantic-model fields, database roles, and release boundaries to those declarations.

Database-backed checking additionally needs a sanitized schema and seed state, or a read-only connection to a representative fixture. Real-DB assertions can constrain row counts, columns, allowed values, and forbidden values. A target without a semantic model, RLS, or release observer may omit that input, but the resulting report must mark the surface unobserved rather than infer conformance.

Specification effort.

The effort depends on how much policy is already machine-readable. A stack with a dbt-style semantic model, explicit tenant columns, structured tool traces, and RLS DDL can transform much of the input mechanically. A stack whose policy lives in prose requires a human to choose a canonical interpretation before testing begins. The tool cannot infer that interpretation without changing the claim from conformance testing to policy discovery. The artifact therefore reports each input as native, mechanically transformed, or synthesized.

The four brownfield targets give a concrete lower bound on this work:

The table inventories 79 adapter traces, not the precision-study denominator. The 75 real-input traces comprise 68 MetricFlow, five Midday, one WrenAI, and one Cube case. The inventory additionally includes one hypothetical WrenAI bypass, two synthesized Cube missing-filter regressions, and one additional Cube clean-policy variant. These four cases are excluded from the primary real-input precision population.

“Script lines” is checked-in transform-script length, not person-hours or an optimized adapter estimate. MetricFlow additionally scans 19 test files and selects 68 of 266 test documents; it skips 43 multi-metric cases, 33 cases outside the chosen model, and 122 macro-dependent cases rather than inventing unsupported IR. Midday concatenates 39 native migrations and transcribes five cited ORM queries. WrenAI maps one required session-property rule. Cube maps one accepted policy and two already-rejected policy fixtures. These measurements show that retargeting is feasible but not push-button: each target requires an explicit decision about what cannot be represented.

Freeze and provenance.

freeze-benchmark hashes detector source, generator source, all mutation specifications, policy and surface YAML, suite input, materialized tasks, package version, and Git commit. A run verifies those hashes before producing evidence. This prevents silent post-freeze tuning, but it does not make a generated suite independent. The paper uses “detector-frozen generated” rather than “blinded” for such cases.

Trusted computing base.

Reference interpreters and adapters are trusted. An 18-operator adapter mutation study makes this risk concrete: 13 mutations hide or weaken real findings, three invent findings, one fails loudly, and one leaves the gate result unchanged. Thus 16/18 tested adapter faults silently corrupt scan output. The current mitigations are schema checks, adapter tests, source mapping, provenance hashes, and explicit evidence levels; independent canary traces and cross-checked gate computation remain future hardening.

Artifact support commands.

The scanner imports SQL and semantic traces, compares dbt-style semantic metadata, optionally executes read-only database checks, and emits gateable findings. The doctor command inventories which policy, trace, database, prompt/tool, release, and CI inputs are wired. Doctor output is a configuration audit, not proof that the application invokes every control correctly.

6 Benchmark Construction

DataPolicyDriftBench contains three synthetic domains. support_saas models tenant-scoped support and revenue analytics; finance_saas models firm, advisor, household, and sensitive-identifier access; analytics_clickhouse models project-scoped product analytics, aggregate-only roles, cohort thresholds, timezones, and materialized-view lineage. They vary schema and policy vocabulary but remain author-controlled fixtures.

Mutation registry.

The registry contains 22 deterministic operators: 12 compiler, five database, two release, and one each for manifest, grammar, and validator. Nine produce over-permissive behavior, eight semantic drift, three lowering violations, and two unsafe releases. Examples include a stale metric alias, forbidden dimension admitted by the grammar, sensitive-column omission, dropped or stale tenant keys, gross/net or unique/count skew, join fan-out, fiscal/calendar mismatch, stale RLS ownership, missing project filters, materialized-view lineage loss, and unsafe small-cohort or sampled release. These are fault hypotheses, not a census of production incidents.

How the 1720 cases are made.

The total combines 170 hand-authored seeded cases and 1550 algorithmic cases:

Seeded YAML matrices specify an operator, principal, request template, typed query, surface skew, and repetition count. The loader expands each matrix row into static cases. For generated case $j$, the algorithm chooses operator $o_j=O[j\bmod |O|]$ from the domain-applicable registry; selects the first non-admin principal; uses a seeded generator to choose allowed or denied metrics, dimensions, and time ranges needed to activate $o_j$; appends -gen to the affected surface version; creates the typed query; and shuffles all materialized tasks with the same seed. It does not mutate arbitrary application source, generate arbitrary SQL text, or mine production traces.

Cycling is balanced within a generated suite, not across the combined benchmark. Support and finance use 14 applicable operators; analytics uses all 22. Once hand-authored matrices and unequal suite sizes are combined, per-operator counts range from 13 to 121. Appendix B reports every operator’s surface, class, and count so coverage density is auditable rather than implied by the total.

Representativeness and mutant accounting.

The registry was authored to cover recurring drift shapes across identity, capability exposure, semantic compilation, database containment, and release. This rationale is tested in two separate ways rather than inferred from 1720/1720. First, 25 cited public faults were screened; 19 could be mapped without reversing their documented direction onto 12 existing operators, while six were excluded as out of scope. These fixtures model the resulting drift shape, not the original vulnerable code path. Second, a spec-blind authoring pass produced 42 cases from contract documents without detector access; PolicyStrata agreed on 39, while three exposed an unspecified cost-combination rule.

The standard generator deliberately emits non-equivalent, well-formed cases, so equivalent and invalid counts are both zero. The runner nevertheless reports killed, survived, equivalent, invalid, clean-control, and false-positive counts separately. This design avoids silently discarding future equivalent or stillborn mutants, but the current zero counts should not be read as evidence that equivalent-mutant selection is solved.

6.1 External Taxonomy Cross-Check

The two checks above still use vocabulary we wrote. A third check measures the registry against a fault taxonomy authored by another group: the eight data-agent vulnerabilities of [28], derived from a systematic audit and evaluated on six data agents including two production cloud analytics services. We mapped each of our 22 operators onto that taxonomy or recorded that it has no counterpart there. The mapping is our judgement and is checked in so it can be disputed; the case counts are derived from the materialized traces.

Two classes are covered and one partially, accounting for 1319 of 1720 cases. V7 is the largest overlap: every operator under it is principal or tenant identity failing to survive a transition, which is the same failure their least-privilege analysis describes. V4 is partial because our semantic oracle compares a reference interpreter against one lowered SQL query, while their case is two backends disagreeing.

The five classes that fall outside each do so because of a v1 boundary stated in Section 3: V1 and V2 precede the typed plan where we start, V5 needs multi-step requests, V6 is a property of the model context rather than of a deployed artifact, and V8 needs cumulative release accounting that v1 declares out of scope. None is a gap discovered after the fact.

The reverse direction is the more interesting one. The remaining 401 cases have no counterpart in that taxonomy because the two threat models differ: their adversary controls the prompt and uploaded data, while our fault needs no adversary at all. A retired alias still advertised to the model, a grammar still admitting a dimension policy has retired, and a validator not yet updated for a newly sensitive column are what an update breaks, not what an attacker induces. Agreement on a fault shape is not evidence that PolicyStrata would detect that fault in the live systems where they observed it.

We therefore cross-check a second independent vocabulary rather than treating one list as a field distribution. LASM organizes 116 surveyed agent-security papers into seven architectural layers and four temporal classes [4]. Our operators occupy three layers—Cognitive, Tool Execution, and Governance—and none occupy Foundation, Memory, Multi-Agent Coordination, or Ecosystem. All 1720 cases score an instantaneous single-request consequence; none model session-persistent, cross-session-cumulative, or stack-propagating state. This second mapping, also our unreviewed judgement, confirms the declared start point and exposes the temporal boundary more sharply. Neither cross-check converts 1720/1720 into recall.

Frozen is not independent.

All 1550 generated cases are verified against a freeze manifest in the final reproduction. Of these, the 750 heldout_v1 cases carry post-detector-freeze provenance; the remaining 800 use the ordinary generated suite name but are still hash-pinned for the final run. Every case shares the same operator taxonomy and generator logic. Freezing makes the exact evaluation reproducible and exposes post-hoc changes; it does not provide third-party authorship or statistical generalization.

7 Evaluation Results

We organize the evaluation by the question each evidence source can answer. Deterministic suites measure fault-model coverage; spec-blind, external-source, and historical-revision suites probe taxonomy dependence; brownfield and deployment-linked checks measure retargeting behavior; intervention and adapter studies test diagnostic assumptions.

RQ1: Does the checker cover its declared fault model?

All 1720 non-clean cases emit a witness, and 80 no-drift controls emit none. The result includes 170 hand-authored cases and 1550 generated cases. Because expected behavior and generated cases share the mutation registry, 1720/1720 is a regression invariant over the implementation, not an estimate of field recall.

RQ2: What do transition contracts catch?

We retain simple point checks as diagnostic ablations, but do not present them as competitors. The stronger comparison is a conventional specification-derived test suite with six checks: tenant predicate presence, rejected forbidden metric, rejected forbidden dimension, row-limit enforcement, blocked release after canonical denial, and golden values for named headline metrics. It is implemented without access to the mutation list. A second comparator performs pairwise differential checks over adjacent surface decisions, following the model-versus-implementation testing pattern used by authorization engines.

The conventional suite’s 141 misses comprise 70 semantic drifts on metrics without golden values, 38 unsafe releases of canonically allowed queries, and 33 containment failures invisible in released values. The pairwise differential misses cases where allow/deny decisions agree while compiler semantics drift; 613 of its misses are compiler-localized semantic drift. All three comparators report 0/80 false positives on the standard clean controls. These results show an observability gap under the benchmark model, not superiority to Margrave, VeriEQL, or a production policy engine, which answer different questions and were not reimplemented.

RQ3: Does non-generator evidence expose misses?

Yes. A spec-blind pass hand-authored three cases for each of 14 support-domain operators after reading the contract and operator descriptions but not detector, simulator, or generator source. The detector killed 39/42. All three misses target the same cost-expansion operator: the public contract lists component costs and a maximum, but does not define their composition, so the author could not construct a reliably over-budget case. Surface attribution matched 42/42, while six predeclared containment guesses were also wrong. This exercise was performed by a non-independent author in the same development environment and is only a proxy for external authorship.

A separate source ledger screened 25 cited public faults from PostgreSQL, Supabase, ClickHouse, Cube, Looker, dbt/MetricFlow, Metabase, Superset, Hasura, and LangChain. Nineteen were mapped to 12 existing operators and all 19 fixtures were killed; six were dropped because their direction or mechanism was outside the model. Exact Git-object replay over three fixes in a private source repository also verified that the relevant source contract was absent before and present after each fix. Two missing-RLS revisions map to app_deny_missing_db_policy; an export-audit omission is reproducible but outside v1. The public artifact reports only aggregate counts, not private revisions, paths, source excerpts, or probe patterns. This replays historical source states, not running vulnerable services, and does not show prevention. Section 6.1 adds the complementary scope check: measured against an independently authored data-agent vulnerability taxonomy, the v1 registry covers two of eight classes and one partially, and 401 of its own cases describe update-induced drift that an attack taxonomy has no reason to name.

No row in this table is an independently operated production study. The separate LASM cross-check maps the same 1720 cases onto a 116-paper architectural taxonomy; it is a scope analysis, not another case suite. The 68 MetricFlow rows are the frozen subset of the 75 brownfield traces, not an additional denominator. The table prevents calling upstream-authored cases an externally operated blind suite, treating historical source probes as vulnerable-service execution, or treating denial probes as field recall.

RQ4: Can the scanner be retargeted?

Static scans targeted MetricFlow, Midday, WrenAI, and Cube. Inputs were labeled native, mechanically transformed, or synthesized. Across 75 traces carrying real SQL content (68 MetricFlow, five Midday, one WrenAI, and one Cube), the initial pass produced one content-level false positive (1.3%) and no newly discovered upstream defect. It did catch Cube’s two already-known broken access-policy fixtures while leaving the valid fixture clean. A fresh MetricFlow checkout at Git object 45dce78641bb reproduced all 68 transformed traces byte-for-byte. Its upstream-authored requests and expected SQL are more independent than generated cases, but the policy bridge remains author-written; 68 fuzz mutations survived because the synthetic bridge role permits every dimension. The five adapter gaps that pass exposed have since been fixed, which is the more useful outcome than the null discovery result: MetricFlow’s adapter-attributable warnings fall from 27 to four, and each survivor is a finding the adapter should report. Running a scanner against code its authors did not write mostly measures the scanner.

Those scans are static, which leaves open whether the checks would notice a real policy that stopped working. One target answers that directly. Midday commits real PostgreSQL row-level security, so we load all 20 CREATE POLICY statements across the six policy-bearing tables in its frozen migrations verbatim into PostgreSQL 18.4 and execute them. Its migrations assume a Supabase base schema they do not commit, so a labeled bridge supplies the roles, auth.uid(), the team-lookup function, and the referenced base tables; checks connect as a non-owner, non-superuser role so that RLS applies rather than being silently bypassed. With Midday’s policies intact, thirteen real-database checks pass and the gate is clean. Replacing one real predicate with USING (true)—the db_rls_old_ownership_field shape applied to real policy text—fails three RLS checks and one state assertion, including a read that is now available unauthenticated, while the five tables whose policies were untouched stay clean. This is real committed policy code enforcing and then failing to enforce, with a negative control; it is not a Midday defect, since its committed predicate is correct, and not its deployed Supabase runtime, which we have not observed.

RQ5: What does a deployment-linked pilot establish?

A maintainer-operated production study verified that the inspected source and deployed source revisions matched; service, route, revision, and deployment identifiers are withheld because the repository and control plane are private. Thirty-three of 36 read-only HTTP boundary probes passed and none failed. Three authenticated reads were skipped because no isolated synthetic production principal exists; checks that could enqueue work or alter state were excluded. On the same source revision, doctor found 33 tools, three roles, six runtime events, and no partial wiring; six SQL traces plus four database checks passed against disposable synthetic PostgreSQL. No customer row was read and no production state was mutated. Thus the study establishes deployment binding, adapter applicability, and selected live denial behavior—not public reproducibility, authenticated cross-tenant behavior, customer-data safety, or effectiveness on unknown faults.

RQ6: Are attributions causal?

Counterfactual repair was evaluated on 120 compound cases per domain. In all 360 cases, repairing the attributed surface removed or moved that first violation, while repairing another surface left it in place. A forced constant-wrong localizer fails this test. The result validates first-transition attribution within the distinct-surface simulator; it does not establish source-code root-cause accuracy.

The bounded reducer reaches 1-minimality under its three edit types on the standard support suites, but reductions are small because generated plans already contain one dimension and few optional fields. Finally, the 18-case trusted-adapter mutation study finds 16 silent corruptions. This negative result sets a practical limit on every scan result: adapter correctness is part of the claim.

Cost.

The frozen artifact run completes in about four seconds on the reported Apple laptop with a prepared environment, producing 1800 traces and 1720 witness files in a 17 MB directory. This is a reproducibility measurement on one machine, not a scaling law.

8 Evaluation Protocol

Every study is deterministic and reports raw counts because the standard suites are enumerated artifacts rather than samples from a defined production distribution. We do not attach confidence intervals to 1720 operator-generated cases.

Scoring.

A non-clean case is killed only when the detector emits a non-clean witness. Survived, equivalent, and invalid cases remain in the denominator accounting rather than being discarded. Clean controls are scored separately. Expected class and expected surface are fixture labels; agreement with them is a regression check, not independent validation. Counterfactual repair is used when making the stronger attribution claim.

Information access.

All comparators receive the same traces but only the fields implied by their design. The conventional suite reads specification-derived properties and selected golden values. The pairwise differential reads surface decisions but not mutation labels, first-transition labels, or witnesses. Point-control ablations inspect only their named surface. PolicyStrata alone evaluates the declared transition contracts; this asymmetry is the feature being tested and is stated rather than hidden.

Provenance separation.

Reports keep five evidence kinds separate: hand-authored synthetic fixtures, operator-generated fixtures, detector-frozen generated fixtures, spec-blind hand-authored fixtures, and public-fault reconstructions. Imported real traces and real-database observations are scanner evidence, not automatically benchmark evidence. A freeze manifest proves source identity, not independence.

Reproducibility.

The final script runs the suites, verifies freeze manifests, emits comparator and ablation reports, and records package and Git versions. Individual scripts reproduce the public-fault, spec-blind, counterfactual, minimization, scalability, clean-control, and adapter studies. No reported study needs an LLM API key. The model-reachability harness has not been run with a model and is excluded from all results.

9 Artifact and Data Availability

The implementation, paper source, benchmark inputs, study scripts, and per-study limitations are available at https://github.com/raintree-technology/policystrata. The repository also provides a Python package, command reference, evaluator guide, expected outputs, freeze manifests, optional database services, and scanner examples. Synthetic data are checked in; public-fault mappings retain their source ledger; brownfield adapters retain field-level native/transformed/synthesized provenance. The paper PDF is built from paper/main.tex, making the package repository the canonical editable source rather than the website.

10 What Remains Unestablished

The maintainer-operated deployment study verifies source-to-deployment binding and selected unauthenticated denial boundaries, but its private identifiers are omitted from the public artifact. It does not exercise an authenticated tenant-to-tenant path because no isolated synthetic production principal is configured. Its deeper semantic, SQL, RLS, and release checks use the deployed source revision with synthetic rows. It therefore does not show public reproducibility, customer-data safety, model choice, retries, caches, concurrent rollout, unknown-fault recall, or independently operated effectiveness. External teams have not operated the study or authored a PolicyStrata-blind suite.

One external target’s real policy text does now execute rather than being read statically, and it fails the right checks when a real predicate is weakened. That covers all 20 policies across the six policy-bearing tables in Midday’s frozen migrations under a bridge we wrote, so it establishes that the containment checks bind to real policy code, not that they generalize to Supabase-managed schema or a deployed runtime.

The next evidence step is therefore an isolated synthetic principal for the three skipped authenticated probes, followed by a suite written by an independent author after detector freeze and an independently operated pilot. The historical replay harness should also advance from exact source-contract probes to executable vulnerable-service replays where dependencies and data fixtures permit.

Technical extensions also remain: same-surface compound mutations, mechanized contract proofs, verifier-backed SQL equivalence, wider witness reduction, sequential and history-aware release, adaptive differencing, writes and side effects, and model-mediated reachability under fixed prompt, model, retry, and refusal settings. Results for these extensions should remain separate from the v1 read-only benchmark.

11 Threats to Validity

Construct validity.

The operator taxonomy may omit real fault shapes, and the simulator may make represented faults easier to detect. The spec-blind cost misses show that even an implemented operator can be underspecified. Finite database states can expose a semantic difference but cannot prove query equivalence.

Internal validity.

Generated inputs, expected labels, and detector behavior share code and concepts. Freeze manifests prevent silent changes but not common design errors. Reference interpreters reduce compiler-oracle coupling, while the adapter mutation study shows that bad normalization can still hide or invent findings.

External validity.

All scored benchmark domains are synthetic. Public-fault cases map outcomes, while three private-source historical cases probe exact pre/post-fix source contracts rather than execute vulnerable services; only aggregate results are public. Brownfield work covers four open-source repositories and uses synthesized bridge values. The one executed-policy result covers all 20 policies across the six policy-bearing tables in Midday’s frozen migrations, but its Supabase runtime is our reconstruction rather than the deployed one, so it shows real policy text enforcing under a bridge we wrote. The maintainer-operated deployment study verifies source-to-deployment binding but withholds private identifiers, uses synthetic data for deep checks, and skips authenticated probes. No customer data or independently operated deployment was evaluated. Two external-taxonomy cross-checks bound the registry against independently authored vulnerability and architectural vocabularies, but both mappings are our judgement and neither taxonomy is a field distribution.

Conclusion validity.

Counts are exact for checked-in deterministic suites but do not estimate a production fault distribution. Zero false positives on generated controls is weak precision evidence because those controls share the simulator. The one-of-75 brownfield figure and 33 passing live probes are more independent but too small, adapter-dependent, and boundary-focused to generalize.

12 Conclusion

PolicyStrata treats a data agent as a policy pipeline whose representations are related but not equal. Its transition contracts separate an upstream lowering error, downstream containment, and final release instead of collapsing them into one pass/fail answer. The artifact covers its declared 22-operator model, exposes gaps missed by specification-derived tests, and emits intervention-checked witnesses for the first failed transition. Spec-blind misses, null brownfield discovery, and silent adapter mutations show where the evidence stops. The result is a reproducible method for policy-drift regression testing. It does not establish production recall and does not replace enforcement.

A Contract Formalization

The formalization fixes terminology for the implemented contracts rather than providing a soundness theorem for arbitrary data-agent deployments.

Let $p$ be a principal and $c$ be runtime context containing request metadata, session state, and deployment versions. Let $X_i$ be the object language at surface $i$, and let $\gamma_i(x)$ interpret object $x \in X_i$ as the concrete operations, data dependencies, or observations it may induce. Let $A_P(p,a,c)$ mean operation or dependency $a$ is authorized by $P^t_{\mathsf{auth}}$. Let $\mathsf{Expose}_i$, $\mathsf{Accept}_i$, and $\mathsf{Release}$ describe actual implementation behavior. Let $E_i(p,x,c)$ be the declared support envelope for surface $i$, and let $L_i:X_i\rightharpoonup X_{i+1}$ be a partial lowering.

Exposure soundness.

$$\mathsf{Expose}_i(p,x,c) \Rightarrow \forall a \in \gamma_i(x), A_P(p,a,c)$$

Declared completeness.

$$E_i(p,x,c) \wedge \forall a \in \gamma_i(x), A_P(p,a,c) \Rightarrow \mathsf{Accept}_i(p,x,c)$$

Authorization-preserving lowering.

$$\mathsf{Accept}_i(p,x,c) \wedge L_i(x)=y \Rightarrow \forall a \in \gamma_{i+1}(y), A_P(p,a,c)$$

Semantic translation validation.

$$\exists D: \mathsf{Obs}(\mathsf{Exec}(L_i(x),D)) \not\approx \mathsf{SpecEval}(x,D)$$

Release conformance.

$$\mathsf{Release}(p,y,\ell,c) \Rightarrow R_P(p,y,\ell,c)$$

Checked detector invariant.

Let $\mathsf{Fail}_i(T)$ mean that the implemented contract decision for surface $i$ rejects trace $T$, and let $\mathsf{UnauthorizedRelease}(T)$ mean the release decision allows an observation rejected by the canonical policy. The implementation checks $$\mathsf{Witness}(T)\Rightarrow \left(\bigvee_i\mathsf{Fail}_i(T)\right) \vee \mathsf{UnauthorizedRelease}(T).$$ This invariant is executable and tested, not proved for arbitrary adapters or implementations.

Why the implementation satisfies the implication.

The detector first searches the ordered contract-decision map. If it returns surface $i$, then by construction $\mathsf{Fail}_i(T)$ is true, so the right side holds. If no surface contract fails, the only branch that emits a non-clean witness checks that release is allowed while the canonical decision denies it. Otherwise the detector returns clean. Classification into over-permissive, lowering, semantic, or release subclasses happens only after one of these two guards. This is a proof sketch over the detector control flow, while the property and finite exhaustive tests check that trace construction supplies the premises as expected.

Completeness boundary.

The 22 operators cover three lowering violations at the compiler, nine over-permissive faults across manifest, grammar, validator, compiler, and database, eight compiler semantic drifts, and two unsafe releases. Completeness is asserted only for well-formed cases instantiated by these operators. No global converse to the checked invariant is claimed.

B Operator Accounting

The table lists the full v1 read-only mutation registry and its frequency in the 1720 non-clean cases. Counts combine all seeded and generated suites; unequal domain sizes explain why operators are not globally balanced.

References

1. Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In 2019 IEEE 32nd Computer Security Foundations Symposium, pages 256–271, 2019.
2. Peter Baile Chen, Devin Yang, Weiyue Li, Fabian Wenz, Yi Zhang, Nesime Tatbul, Michael Cafarella, Çağatay Demiralp, and Michael Stonebraker. BEAVER: An enterprise benchmark for text-to-SQL. arXiv preprint arXiv:2409.02038, 2024.
3. Zheng Chen, Hanqing Liu, Duling Xu, Dong Dong, Jialin Li, Bangzheng Pu, and Jidong Zhai. Cordon: Semantic transactions for tool-using LLM agents. arXiv preprint arXiv:2606.17573, 2026.
4. Kexin Chu. A systematic survey of security threats and defenses in LLM-based AI agents: A layered attack surface framework. arXiv preprint arXiv:2604.23338, 2026.
5. Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and Andrew Wells. How we built cedar: A verification-guided approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024.
6. Yixin Dong, Charlie F. Ruan, Yaxing Cai, Ruihang Lai, Ziyi Xu, Yilong Zhao, and Tianqi Chen. Xgrammar: Flexible and efficient structured generation engine for large language models. arXiv preprint arXiv:2411.15100, 2024. MLSys 2025.
7. Kathi Fisler, Shriram Krishnamurthi, Leo A. Meyerovich, and Michael Carl Tschantz. Verification and change-impact analysis of access-control policies. In Proceedings of the 27th International Conference on Software Engineering, pages 196–205, 2005.
8. Saibo Geng, Hudson Cooper, Michał Moskal, Samuel Jenkins, Julian Berman, Nathan Ranchin, Robert West, Eric Horvitz, and Harsha Nori. Jsonschemabench: A rigorous benchmark of structured outputs for language models. arXiv preprint arXiv:2501.10868, 2025.
9. Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang. Verieql: Bounded equivalence verification for complex sql queries with integrity constraints. Proceedings of the ACM on Programming Languages, 8(OOPSLA2), 2024. Also available as arXiv:2403.03193.
10. Nafiseh Kahani, Masoud Barati, and Diana Addae. Runtime compliance verification for AI agents. arXiv preprint arXiv:2606.19242, 2026. Introduces C-Trace, a compliancetrace runtime enforcement framework.
11. Ðorđe Klisura, Joseph Khoury, Ashish Kundu, Ram Krishnan, and Anthony Rios. Role-conditioned refusals: Evaluating access control reasoning in large language models. In Findings of the Association for Computational Linguistics: EACL 2026, pages 6018–6034, Rabat, Morocco, 2026. Association for Computational Linguistics. doi: 10.18653/v1/2026.findings-eacl. 316. Also available as arXiv:2510.07642.
12. Fangyu Lei, Jinxiang Meng, Yiming Huang, Junjie Zhao, Yitong Zhang, Jianwen Luo, Xin Zou, Ruiyi Yang, Wenbo Shi, Yan Gao, Shizhu He, Zuo Wang, Qian Liu, Yang Wang, Ke Wang, Jun Zhao, and Kang Liu. DAComp: Benchmarking data agents across the full data intelligence lifecycle. arXiv preprint arXiv:2512.04324, 2025.
13. Ido Levy, Ben Wiesel, Sami Marreed, Alon Oved, Avi Yaeli, and Segev Shlomov. ST-WebAgentBench: A benchmark for evaluating safety and trustworthiness in web agents. arXiv preprint arXiv:2410.06703, 2024.
14. Jinyang Li, Binyuan Hui, Ge Qu, Jiaxi Yang, Binhua Li, Bowen Li, Bailin Wang, Bowen Qin, Rongyu Cao, Ruiying Geng, Nan Huo, Xuanhe Zhou, Chenhao Ma, Guoliang Li, Kevin C. C. Chang, Fei Huang, Reynold Cheng, and Yongbin Li. Can LLM already serve as a database interface? a BIg bench for large-scale database grounded text-to-SQLs. arXiv preprint arXiv:2305.03111, 2023.
15. Tianxiao Li, Yixing Ma, Haiquan Wen, Zhenglin Huang, Qianyu Zhou, Zeyu Fu, and Guangliang Cheng. Safe multiagent behavior must be maintained, not merely asserted: Constraint drift in LLM-based multi-agent systems. arXiv preprint arXiv:2605.10481, 2026.
16. Yixi Lin, Jiangrong Wu, Yuhong Nan, Xueqiang Wang, Xinyuan Zhang, and Zibin Zheng. Agentraft: Automated detection of data over-exposure in LLM agents. arXiv preprint arXiv:2603.07557, 2026.
17. Ruiying Ma, Shreya Shankar, Ruiqi Chen, Yiming Lin, Sepanta Zeighami, Rajoshi Ghosh, Abhinav Gupta, Anushrut Gupta, Tanmai Gopal, and Aditya G. Parameswaran. Can AI agents answer your data questions? a benchmark for data agents. arXiv preprint arXiv:2603.20576, 2026.
18. Evan Martin and Tao Xie. A fault model and mutation testing of access control policies. In Proceedings of the 16th International Conference on World Wide Web, pages 667–676, 2007.
19. Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, and Somesh Jha. Formal policy enforcement for real-world agentic systems. arXiv preprint arXiv:2602.16708, 2026. FORGE; arXiv v3 describes a Datalog reference monitor, observability service, and aspect weaver.
20. Zongrui Peng, Jingzhou Fu, Zhiyong Wu, Jie Liang, Xiangdong Huang, Dalong Shi, and Yu Jiang. Beacon: Detecting broken access control vulnerabilities in dbmss via system catalog consistency validation. Proceedings of the ACM on Programming Languages, 10(OOPSLA1):905–933, 2026. doi: 10.1145/3798232.
21. Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, pages 151–166. Springer, 1998. doi: 10. 1007/BFb0054170.
22. PostgreSQL Global Development Group. Postgresql documentation: Row security policies. https://www.postgresql.org/ docs/current/ddl-rowsecurity.html, 2026. Accessed 202606-24.
23. Tzafrir Rehan. Test-driven ai agent definition (TDAD): Compiling tool-using agents from behavioral specifications. arXiv preprint arXiv:2603.08806, 2026.
24. Torsten Scholak, Nathan Schucher, and Dzmitry Bahdanau. Picard: Parsing incrementally for constrained autoregressive decoding from language models. arXiv preprint arXiv:2109.05093, 2021.
25. Tianneng Shi, Jingxuan He, Zhun Wang, Hongwei Li, Linyu Wu, Wenbo Guo, and Dawn Song. Progent: Securing ai agents with privilege control. arXiv preprint arXiv:2504.11703, 2025.
26. Charlie Summers and Eugene Wu. Data flow control: Data safety policies for ai agents. arXiv preprint arXiv:2606.05679, 2026.
27. Andrew Tremante, Yang He, Rocky Klopfenstein, Yuepeng Wang, Nina Narodytska, and Haoze Wu. Spotit+: Verificationbased text-to-SQL evaluation with database constraints. arXiv preprint arXiv:2603.04334, 2026.
28. Kuncan Wang, Ziting Wang, Peizhuo Lv, Haoyang Li, Guoliang Li, Gao Cong, and Wei Dong. Data agents under attack: Vulnerabilities in llm-driven analytical systems. arXiv preprint arXiv:2606.08661, 2026.
29. Brandon T. Willard and Rémi Louf. Efficient Guided Generation for Large Language Models. arXiv preprint arXiv:2307.09702, 2023.
30. Shunyu Yao, Noah Shinn, Pedram Razavi, and Karthik Narasimhan. τ -bench: A benchmark for tool-agentuser interaction in real-world domains. arXiv preprint arXiv:2406.12045, 2024.
31. Tao Yu, Rui Zhang, Kai Yang, Michihiro Yasunaga, Dongxu Wang, Zifan Li, James Ma, Irene Li, Qingning Yao, Shanelle Roman, Zilin Zhang, and Dragomir Radev. Spider: A largescale human-labeled dataset for complex and cross-domain semantic parsing and text-to-sql task. In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, 2018.
32. Shenghan Zheng and Qifan Zhang. Agentrfc: Security design principles and conformance testing for agent protocols. arXiv preprint arXiv:2603.23801, 2026. Describes AgentConform for protocol IR extraction, TLA+ checking, and live SDK trace replay.
33. Ruiqi Zhong, Tao Yu, and Dan Klein. Semantic evaluation for text-to-SQL with distilled test suites. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 396–411, Online, 2020. Association for Computational Linguistics. doi: 10.18653/v1/ 2020.emnlp-main.29. URL https://aclanthology.org/2020. emnlp-main.29/.