adversarial validation · attestral validate
Reachability, not just findings.
Every other scanner stops at "this looks risky." Attestral takes the attack path it assembled from your system model, walks it over the model's own edges, and shows it is reachable in the modeled design - entry, pivot, impact, stage by stage - then chains the walked path to a tamper-evident evidence chain. A static finding is a claim about one config block. A walked, chained path names every rung and the boundaries it crosses.
What this claims. Reachability is computed over the capability your design declares, treated as a sound over-approximation. It is a necessary, not sufficient, condition for a working attack: it does not model whether the agent follows an injection, or whether a guardrail or human approval sits in the path. We report feasibility over the modeled graph, never proof that an attacker succeeds.
Watch the path get walked. Then try to break it.
This is a real fleet: a support agent with a web fetcher, a ticket reader, a shell, and a deploy tool. One tool description carries a hidden instruction to read ~/.ssh/id_rsa and post it out. Hit Run validation and watch the path get walked. Then toggle a server off and watch it go away: remove any one rung and the path is no longer reachable. That is the whole point. The fix is one toggle, and now you can see it.
The fleet (toggle any server, then re-run). Capability tags mirror the MCP ingester; the walk mirrors attestral/paths.py and attestral/redteam.py.
The proof is chained, so an auditor can verify it offline.
Each proof commits to a SHA-256 hash chain exactly as attestral verify does: entry N hashes its canonical JSON together with the hash of entry N-1, from a zero genesis. The head is the integrity commitment for the run. Recomputed live below from the proofs above. Tamper with one entry and the whole chain gives it away.
A waived path is never deleted, only marked. A reachable path that you accept and document stays in the chain with its justification, so the record shows what was known and when. That is the difference between an audit record and a scan log.
The same thing, in your terminal.
Real output from attestral validate examples/vulnerable-agent. The browser engine above is a faithful port; the CLI is the source of truth, and it also writes the proof report and the evidence chain when you pass -o.
Adversarial validation (1 reachable)
ATL-RT-INTERNAL Reachable in the modeled design: a prompt injection can reach exfiltration
1. entry: jira - ingests untrusted input via saas_data
2. entry: web - ingests untrusted input via network
3. pivot: deploy - runs code via shell
4. pivot: shell - runs code via shell
5. impact: web - exfiltrates via network
boundaries: agent_runtime
verdict: traversable
fix: Break the chain: remove any one rung. Drop the code-execution capability on deploy...
$ attestral validate examples/vulnerable-agent -o proof --fail-on-reachable
wrote proof.md · proof.json
$ attestral verify proof.json
chain VALID
New · attestral validate --remediate
It verifies the fix, not just the flaw.
A finding tells you something is wrong. Attestral goes further: for each reachable path it names the minimal fix and verifies it by re-synthesis - it strips the rung, rebuilds the whole system model, and re-runs the walk to confirm the path is actually gone from the graph. Not "this is risky," but "here is the one change, and here is the re-synthesis that removes the path." It ranks the fixes by how far each drops your worst agentic risk, scored as an AARS (Agentic AI Risk Score, 0–10), so the highest-leverage change comes first.
Verified remediations (2)
Scope or remove the outbound channel on web
verify: strip network/messaging, re-synthesize -> PROVEN: closes every path
posture: worst agentic risk AARS 10.0 -> 7.6
Remove code execution (shell) from deploy, shell
verify: strip shell, re-synthesize -> PROVEN: closes every path
posture: worst agentic risk AARS 10.0 -> 9.3
--action-space goes wider still: it enumerates the tool-call sequences the fleet can be induced into, not just the one collapsed chain, the behavioral surface a per-config scanner never sees.
Three tiers. One walked-path schema.
All three tiers ship: symbolic shows the path is reachable, generative drafts the predicted exploit, and executed replays it in a sandbox harness. Each builds on the same walked path and degrades gracefully: the tier you have installed is the tier you get, and a missing key or extra is never an error. Execution against your own live target stays gated.
Show the path is reachable
Walk each attack path over the model's own edges. Deterministic, zero-dependency, no execution, no network. It shows the path is reachable over the model's own edges and names every rung. A design with no complete path yields no reachable path, which is itself an attestable result.
shipping nowDraft the payload
With --generate, an LLM turns a reachable path into the predicted artifact that would traverse it: the injection shape, the predicted tool-call sequence, the transcript it expects. No live target is touched. Labeled predicted, not executed.
Capture the transcript
With --execute, Attestral replays the reachable path through its own sandbox harness with a planted canary, moving the marker from a stub secret store to a captured sink and recording the transcript. The harness ships today; execution against your own fingerprinted live target stays gated.
Scope, by design
The symbolic tier never touches a live system at all. It reasons over the model you already attested. The executed tier will run only against a target whose fingerprint matches that attested model and only with explicit authorization, in a sandbox, moving planted canaries rather than real secrets. Attestral surfaces the reachable attack paths in a design you own so you can close them. It is not a point-it-at-any-endpoint attack tool, and it never will be.
New · attestral validate --execute
Tier 2: watch the canary walk out.
The symbolic tier shows the path is reachable; the sandbox tier replays it. Attestral runs the reachable path through its own stub tools with a planted canary, moving the marker from a fake secret store to a captured sink. No real system, no real secret, no network, just a demonstration of the mechanics end to end, with the transcript to show for it.
Harness only. Every marker is a harmless canary; nothing real is touched. The transcript is real, the target is not, and execution against your own live agent stays gated.
Does this make you flinch?
Point it at your own fleet. If the walked path makes you reach for the config, that is the signal a static finding could never give you. It reads only what you point it at, runs on your laptop, and sends nothing anywhere.