# 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.
Part of [CAR](https://github.com/Parslee-ai/car) -- see the main repo for full documentation.