# 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.
## Admission into durable state
`admission` decides what becomes durable reusable state — a memory, a skill, a
routing rule, a retained failure. **This is not `car_engine::admission`**, which
runs before execution and decides whether actions may *run*. Different objects:
CAR has a mature execution gate and, before this, no state gate at all
(`gate_skill_candidates` is the one exception, and it covers skills only).
Admission needs two things, and either alone is insufficient:
```rust
use car_verify::{admit_state, CommitAuthority, EvidenceRequirement, OwnershipTable,
SelfCommit, StateCandidate, StateSurface, SurfaceRule};
let table = OwnershipTable::new().with(SurfaceRule {
surface: StateSurface::Memory,
produced_by: CommitAuthority::Execution, // who may produce
committed_by: CommitAuthority::Review, // who may commit
self_commit: SelfCommit::Forbidden, // producer may never self-commit
requires: vec![EvidenceRequirement::new("tests")],
});
let candidate = StateCandidate::new(StateSurface::Memory, "fact:deploy-target",
CommitAuthority::Execution)
.committed_by(CommitAuthority::Review)
.with_verdicts([verdict]);
assert!(admit_state(&table, &candidate).admitted);
```
Evidence without authority is a candidate nobody accountable accepted; authority
without evidence is a rubber stamp. Refusals accumulate rather than
short-circuit, so one call surfaces every problem.
`SelfCommit` makes the central hazard — the producer committing its own work —
an explicit per-surface policy rather than an accident. A blanket ban is the
wrong target, since requiring independent review for every low-risk update makes
review a bottleneck, and bottlenecks get disabled. `WithPassingEvidence` permits
self-commit only once evidence passes. Note the degenerate case: that setting
with an empty requirement list is an ungated surface, and `is_ungated()` /
`ungated_surfaces()` report it rather than letting it look governed.
Fail-closed throughout — a surface with no rule refuses everything rather than
admitting everything, so an empty table is maximally strict.
The module stores nothing and commits nothing; it is the decision procedure a
caller consults before writing. Its first caller is
`car_memgine::MemgineEngine::try_ingest_fact`, behind the `memory.add_fact`
daemon surface — configured with `memory.set_admission_table`.
Two properties of that wiring: **no table installed means the gate is off**
(engaging a fail-closed gate implicitly would refuse every memory write on every
existing deployment, and it also means facts written before a table existed are
never re-examined), and **only the externally-authored path is gated** — the
engine's own derived writes from consolidation, reflection, and distillation
stay on the ungated `ingest_fact`, since they are not the threat model and would
deadlock the runtime against its own rules.
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.