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.

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.

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?

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 VerifierVerdicts that decided its outcome, which is what makes a retained failure citable rather than merely recorded:

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.

Part of CAR -- see the main repo for full documentation.