New · adversarial validation · attestral validate
Proof, not 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 proves it holds - entry, pivot, impact, stage by stage - then commits the proof to a tamper-evident evidence chain. A static finding is arguable. A walked, chained proof of the exact path is not.
Watch a proof render. 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 the proof die: remove any one rung and the exploit is gone. 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 proof is never deleted, only marked. A proven path that you accept and document stays in the chain with its justification, so the record shows what was known and when. That is what makes it audit-grade rather than 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 proven)
ATL-RT-INTERNAL Proven traversable: 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-proof
wrote proof.md · proof.json
$ attestral verify proof.json
chain VALID
New · attestral validate --remediate
It proves the fix, not just the flaw.
A finding tells you something is wrong. Attestral goes further: for each proven 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 proof to confirm the path is actually gone. Not "this is risky," but "here is the one change, and here is proof it closes it." It ranks the fixes by how far each drops your worst agentic risk score, 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 proof schema.
All three tiers ship: symbolic proves the path, generative drafts the exploit, and executed replays it in a sandbox harness. Each builds on the same proof 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.
Prove the path holds
Walk each attack path over the model's own edges. Deterministic, zero-dependency, no execution, no network. It proves the path is structurally traversable and names every rung. A design with no complete path proves nothing, which is itself an attestable result.
shipping nowDraft the payload
With --generate, an LLM turns a proven path into the concrete 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 proven 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 proves the flaws 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 proves the path holds; the sandbox tier replays it. Attestral runs the proven 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 proof 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 proof 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.