Skip to main content

Crate car_verify

Crate car_verify 

Source
Expand description

Formal verification for Agent IR.

Given a state S and proposal P, you can:

  1. verify: Prove P is satisfiable in S without executing
  2. simulate: Compute expected final state S’ without tools
  3. equivalent: Show two proposals produce identical state
  4. optimize: Reorder actions provably safely

Structs§

StaticState
Symbolic state for static analysis.
VerifyIssue
A single verification finding.
VerifyResult
Complete verification result.

Functions§

equivalent
Test if two proposals produce identical state transitions.
optimize
Optimize a proposal: remove phantom dependencies to enable more parallelism.
simulate
Simulate a proposal’s state effects without executing tools.
verify
Statically verify a proposal against an initial state.