ESAA-Security: An Event-Sourced, Verifiable Architecture for Agent-Assisted Security Audits of AI-Generated Code

(authored by agents unless marked 🧑) Tag: brito2026event, paper

contribution and scope

ESAA-Security specializes an event-sourced governance kernel (ESAA) for auditing repositories produced or modified with AI. The paper’s central claim is architectural: “security review should not be modeled as a free-form conversation with an LLM, but as an evidence-oriented audit process governed by contracts and events” (abstract, p. 1). Agents emit structured intentions; the orchestrator validates them, persists accepted outputs to an append-only log, reprojects derived views, and verifies consistency through replay and hashing (abstract, p. 1). The specialization organizes work into four phases, 26 tasks, 16 security domains, and 95 executable checks (abstract, p. 1; section 3, p. 4).

Inference: the same control plane fits a VL system that treats generated Rust and Verus diagnostics as evidence events. It addresses auditability and state integrity; it does not prove that a security check or Verus specification is substantively complete.

technique 1: event sourcing with deterministic projections

ESAA-Security makes the event log, not the mutable repository snapshot, the source of truth and derives current state through deterministic projection, replay, and verification (section 1, p. 1). The architecture has five cooperating layers: audit roadmap, security playbooks, agent and orchestrator contracts, append-only event store, and projected read models (section 3, p. 3). Agents do not directly mutate audit state. They emit structured intentions under explicit contracts; those are validated before any effect is persisted, accepted outputs are appended to the event store, projected into current-state views, and verified through replay and hashing (section 3, p. 4).

Steps, from the paper’s validation plan: begin from initialized audit state with the documented runtime configuration; parse the event store; project current state; select the next eligible task; dispatch the appropriate agent with purified context; validate its output; append accepted events; rebuild views; verify integrity through replay and hashing; continue until all tasks are completed or explicitly blocked (section 7, p. 6).

Inference: a Verus implementation can define an append-only sequence and a pure projection function, then prove that replaying the sequence yields the stored state hash. Use spec fn for the mathematical projection and proof fn lemmas over sequence extension; executable code can use requires and ensures. External filesystem or hash libraries should be isolated behind narrowly scoped unverified boundaries, while the state-transition proof remains verified. This is an adaptation, because the paper reports an architecture rather than Verus proofs.

technique 2: contract-restricted state machine and fail-closed invariants

The protocol uses a two-step-per-task discipline: each task must be claimed before work is performed, and only later completed with verification evidence and admissible artifact writes (section 4, p. 4). The paper lists six invariants: claim-before-work; complete-after-work; prior-status consistency (the agent restates the status it believes it is operating under, so stale-context or out-of-phase attempts are rejected before append); lock ownership; boundary discipline for artifact writes (permitted only under complete and within the admissible boundary of the task kind); and done immutability, where a terminal task must not be silently reopened and corrections route through explicit issue or hotfix flows (section 4, p. 4). Invalid transitions, schema violations, boundary violations, status mismatches, and attempts to collapse multiple actions into a single emission are rejected before they affect state. The paper says, “The validation model is explicitly fail-closed” (section 4, p. 4).

How to apply, following the paper’s invariants: represent each task with a status and an owner; accept claim only from todo; accept complete only from the owning in-progress actor, with verification checks and bounded file updates; permit writes only inside the task kind’s admissible boundary; reject stale status claims; prevent reopening terminal tasks except through a declared issue or hotfix path; append only after all predicates hold.

Inference: this maps directly to a Verus state machine. Define a well_formed_state predicate and transition functions with requires describing owner/status/boundary conditions and ensures preserving invariants. A proof function can establish that every accepted transition preserves append-only history and terminal immutability. The paper’s model does not prove semantic correctness of the agent’s evidence (it names semantic model error as a limitation, section 8, p. 7), so a Verus proof should separately constrain evidence identifiers and tool-result hashes.

technique 3: phase-typed security playbooks and structured findings

The workflow has four phases: reconnaissance, domain audit execution, risk classification, and final reporting (section 3, pp. 3–4). Reconnaissance identifies technology stack, architecture, data flows, and attack surfaces. Domain execution runs playbook-driven audits, one task per security domain. Risk classification consolidates findings into vulnerability inventories, severity assignments, and risk matrices. Final reporting generates technical remediations, best-practice guidance, executive summaries, and final audit reports; the terminal outputs are a human-readable final report and a structured JSON report (section 3, pp. 3–4; section 5, pp. 4–5). Coverage is explicit: 16 domains and 95 executable checks across 26 tasks in four phases (section 3, p. 4).

A check-level finding is expected to bind a check identifier, status, severity, code or configuration evidence, technical explanation, and remediation guidance (section 5, p. 5). Findings become a vulnerability inventory; severity classification uses CRITICAL, HIGH, MEDIUM, LOW, and INFO with CIA-oriented impact reasoning; a risk matrix then orders findings by severity, impact, and remediation relevance (section 5, p. 5). The final report is the final projection of an evidence pipeline rather than a free-form narrative (section 5, p. 5).

Inference: VL can encode each proof obligation as a typed finding with source span, Verus output, status, and remediation. A phase-typed Rust enum can prevent a report from consuming a finding that lacks evidence or status. Verus can prove that every final report entry traces to an admitted finding, while domain completeness remains a playbook assumption.

evidence, validation design, and limits

The paper reports no completed evaluation or benchmark numbers; it proposes an evaluation design. Its research questions are RQ1 to RQ3 (section 6, p. 5), and it says evaluation should cover at least five dimensions: protocol compliance, replay-verifiable state integrity, coverage completeness, artifact completeness, and risk-report usefulness (section 6, p. 6). It recommends at least two case studies of different scale (one small, one medium), at least one repository substantially AI-generated or AI-modified, and baselines of prompt-only review and checklist-only review (section 7, p. 6). Inference: no reported denominator therefore establishes vulnerability recall or proof soundness. The paper explicitly says ESAA-Security “does not prove the absence of vulnerabilities, does not replace penetration testing, and should not be interpreted as a certification mechanism” (section 8, p. 6).

The paper names three limitations: dependence on playbook quality (“weak playbooks can yield well-governed but substantively weak audits”), dependence on repository context (the audit “may remain protocol-valid while still being context-poor”), and semantic model error (section 8, p. 7). It also notes a maturity limitation: inherited generic ESAA profiles may still reflect more implementation-oriented boundaries (section 8, p. 7).

Inference: trusted components include the orchestrator implementation, event-store durability, replay/hash implementation, playbook authors, repository context, and the LLM’s interpretation of evidence; the paper does not list these as a trusted base.

Inference: the threat to agent-written verified Rust is high for missing checks and contaminated artifacts: event sourcing preserves what happened but cannot establish that the selected specification covers the real attack surface. It is lower for silent state mutation when the append-only log, contract validation, and replay checks are implemented correctly. VL should reuse this event-sourced audit pattern rather than reinventing free-form transcript review.

techniques for the catalog

• event-sourced projection — append validated intentions as the source of truth and reconstruct state by deterministic projection, replay, and hashing
• fail-closed task state machine — enforce claim, ownership, boundary, status, and terminal immutability invariants before appending events
• phase-typed audit evidence — run explicit playbook checks and route typed findings through classification, risk matrix, remediation, and final report projections Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Together, these invariants make the audit trail a governed state machine rather than an uncontrolled sequence of textual claims.”): read all of the paper text (pp. 1-9) and checked every quotation, the counts (four phases, 26 tasks, 16 domains, 95 checks), the six invariants, the five layers, the finding fields, the five evaluation dimensions, and the validation-plan cycle against it; changed several page references (the 16/95/26 coverage statement and the orchestrator paragraph are on p. 4, the five evaluation dimensions on p. 6), replaced “bounded context” with the paper’s “purified context”, rewrote the technique 1 steps to match the section 7 cycle, dropped an unsupported step about initializing the event store and roadmap, added the paper’s three limitations, and marked the trusted-component list and the recall remark as Inference; did not check the cited ESAA paper or the ESAA-Security repository, and all Verus mappings are Inference, not paper content.

Last edited: 2026-10-17