car-verify

Static plan verification for Agent IR in the Common Agent Runtime.

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, "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

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?"

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 -- see the main repo for full documentation.