# car-verify
Static plan verification for Agent IR in the [Common Agent Runtime](https://github.com/Parslee-ai/car).
Deterministic graph and dataflow algorithms — no solver, no proof term. The checks
differ in strength (some are decision procedures, some are heuristics, some sample),
and every result carries a `VerificationEvidence` bundle naming what each check did
and did not establish. Read that rather than trusting `valid` alone; the module docs
in `src/lib.rs` spell out the taxonomy and the known blind spots.
That taxonomy is also carried in the data. Every `VerifyIssue` and `CheckRecord`
tags itself with an `EvidenceTier` — `DecisionProcedure`, `Heuristic`, or
`Sampled` — so a caller can tell an exact set-membership failure from the
`count >= 3` loop rule without recognising the message string, and modules whose
findings all share one tier expose `report.evidence_tier()`.
`DecisionProcedure` means the check **decides the property it reports over the
inputs it was given**. It is not a proof, not a soundness claim, and not a
prediction that the plan will run. Whether those inputs describe what actually
happens at runtime is a separate axis — the forward walk applies only what an
action *declares* — and that axis stays in `cannot_verify` / `assumptions` /
`untested_regions`, where it already was.
The tiers are kinds, not grades: `EvidenceTier` derives no `Ord`, because
`Heuristic` and `Sampled` fail in different directions and neither is
categorically stronger. Compare tiers by equality or match on them; filtering
findings down to `DecisionProcedure` throws away the only signal this crate has
for the things no decision procedure here covers.
Why carry the tier at all rather than leaving it in prose:
[`docs/proposals/shepherd-substrate-adoption.md`](../../../docs/proposals/shepherd-substrate-adoption.md),
"What we should also steal: how to state a formal claim" — the argument is that
a stronger claim ships honestly by being *tiered and attached to each run*,
which is the half CAR's existing "never say formal, never say sound" discipline
did not cover.
## What it does
Statically analyzes action proposals without executing them. Verifies precondition
satisfiability, detects write conflicts, checks state dependency availability, and flags
repeated tool calls (loop detection). Can also simulate final state, test proposal
equivalence, and optimize DAG parallelism by pruning phantom dependencies.
## Usage
```rust
use car_verify::{verify, simulate, equivalent, optimize};
use car_ir::ActionProposal;
let result = verify(&proposal, Some(&initial_state), Some(&tools), 30);
assert!(result.valid);
let final_state = simulate(&proposal, None);
let optimized = optimize(&proposal);
```
## Monte Carlo rollout
`simulate` answers "what state does this plan leave behind, assuming every
dispatched tool succeeds?" `simulate_monte_carlo` answers the question an
operator actually asks before running a plan against production: "how often does
this work, and when it doesn't, what breaks first?"
```rust
use car_verify::{simulate_monte_carlo, MonteCarloConfig};
// Per-tool empirical success rates, from what actually happened. The daemon
// records a trajectory per execution; `Runtime::tool_feedback(30)` derives
// dispatch-conditional rates over the last 30 days.
let rates = runtime.tool_feedback(30).unwrap().tool_success_rates;
let mc = simulate_monte_carlo(&proposal, None, &rates, Some(&goal), &MonteCarloConfig::default());
println!("P(goal) = {:?}", mc.p_goal_reached);
println!("tool calls p95 = {}", mc.tool_calls.p95);
// Which failure hurts most, rather than which is most likely.
let worst = mc.action_outcomes.iter()
.max_by(|a, b| (a.p_failed * a.mean_blast_radius)
.partial_cmp(&(b.p_failed * b.mean_blast_radius)).unwrap());
```
The rollout kernel is the same one `simulate` uses, with one change: a
`tool_call` succeeds with probability `p` rather than always. Everything else —
pre-dispatch gating on preconditions and state dependencies, and the cascade
where a failure starves its dependents — is inherited, so the two agree exactly
when every rate is 1.0 (there is a test asserting this).
Sampling is a seeded SplitMix64 stream rather than `rand`, keeping this crate at
`car-ir` + serde and making runs byte-for-byte reproducible from
`MonteCarloConfig::seed`.
Deliberately **not** modelled, matching `simulate`'s documented scope:
`failure_behavior`, partial effects, and correlated failure — draws are
independent, so a plan calling one flaky tool repeatedly reads more
optimistically here than it behaves when that tool's service is down. See the
`montecarlo` module docs for the full boundary.
## External verifiers
`VerificationEvidence` describes the checks this crate runs. `verifier` opens that
bundle to checks it does not own — a test suite, a type checker, a browser
evidence collector, a human — so their verdicts land in the *same*
`VerificationEvidence.checks` vocabulary instead of travelling as prose.
```rust
use car_verify::{admit, AdmissionOutcome, EvidenceRequirement, EvidenceTier,
VerifierDescriptor, VerifierVerdict};
// "The test suite must pass, and a model judge's opinion does not count as one."
let req = EvidenceRequirement::new("tests").accepting([EvidenceTier::DecisionProcedure]);
let verdict = VerifierVerdict::pass(VerifierDescriptor::binding("cargo_test", "tests"));
let decision = admit(&[req], &[verdict]);
assert_eq!(decision.outcome, AdmissionOutcome::Admit);
// decision.records folds straight into VerificationEvidence.checks
```
Three orthogonal axes, deliberately not collapsed into one: `EvidenceTier` (how
strong is this check?), `VerifierAuthority` (whose word is this — `Advisory`,
`Binding`, `Operator`?), and `VerifierCost` (what does running it cost?). `admit`
ignores cost entirely and treats authority as a kind of claim, not a grade.
The load-bearing default: a passing `Operator` verdict does **not** satisfy a
`"tests"` requirement unless that requirement opts in with `operator_override`. A
human clicking approve is a decision to proceed, not a demonstration that the
suite passes. Fail-closed throughout — `Inconclusive` and `Skipped` never
satisfy, and a requirement with no matching verdict is unmet rather than
vacuously true.
This module runs nothing; it defines the vocabulary and the fold. Invoking
verifiers belongs to whoever owns the process boundary (`car-engine`'s
`AdmissionGate`, the `supervision.*` surface, a CI harness).
## Attempt ledger
`attempt` answers the question a planner needs *before* it proposes: have we
already tried an equivalent approach under equivalent assumptions, and has
anything changed since?
```rust
use car_verify::{Attempt, AttemptAdvice, AttemptLedger, FailureClass};
let mut ledger = AttemptLedger::new();
ledger.record(
Attempt::failure("a1", "retry upload with backoff",
["endpoint is v1".into(), "token is valid".into()],
FailureClass::ToolError, "503 from the endpoint")
.retry_when(["endpoint is v1".into()]),
);
// Same assumptions — a decided dead end.
assert!(matches!(
ledger.consult("retry upload with backoff", ["endpoint is v1", "token is valid"]),
AttemptAdvice::KnownFailure { .. }
));
// The declared retry condition changed — worth trying again.
assert!(matches!(
ledger.consult("retry upload with backoff", ["endpoint is v2", "token is valid"]),
AttemptAdvice::RetryUnblocked { .. }
));
```
Matching is exact over normalised labels — it does **not** decide semantic
equivalence, and a caller that invents a fresh label per attempt honestly gets
`Untried` every time. `SimilarFailure` is a distinct answer for "relevant history
exists but the recorder declared no retry condition", kept separate so it is
rounded neither to a hard block nor to a clean slate.
Advisory, never a gate: a `KnownFailure` is a strong reason to pick another
branch, not a prohibition. Blocking belongs to the admission gates, which have
the authority model for it.
### Verified exclusions
An `Attempt` carries the `VerifierVerdict`s that decided its outcome, which is
what makes a retained failure *citable* rather than merely recorded:
```rust
let attempt = Attempt::failure("a1", "reduce via P13", [],
FailureClass::Verification, "counterexample found")
.with_verdicts([VerifierVerdict::fail(
VerifierDescriptor::binding("counterexample_check", "proof"),
"24-vertex witness disproves the reduction",
)]);
assert!(attempt.is_verified_exclusion());
// ledger.verified_exclusions() lists only these — the routes foreclosed on evidence
```
A failure backed by a verifier with authority to decide has foreclosed a route.
A failure backed by nothing, or by an advisory opinion, is a note about one bad
afternoon — it still steers `consult`, but it is not evidence, and
`verified_exclusions()` omits it. `AttemptAdvice::KnownFailure` reports which
kind it found via its `verified` flag.
The distinction matters because a route abandoned on evidence and a route
abandoned on vibes read identically once written into prose. Keeping them apart
in the data is what lets a later decision to change course cite *why* — the
input a contract amendment names as its justification.
Design and the wider audit this came from:
[`docs/proposals/argus-control-layer.md`](../../../docs/proposals/argus-control-layer.md).
Part of [CAR](https://github.com/Parslee-ai/car) -- see the main repo for full documentation.