Validating a Stochastic System

Here’s the testing toolbox for a system with random input. Three layers, plus a fourth for when a property matters enough to prove.

Layer 1: Example tests

assert_eq!(decide(&reports), Decision::Brake) has a place: golden scenarios with noise disabled, pinning the deterministic core. But an agent asked for “tests” usually produces only this layer, often by seeding or disabling the randomness so the suite passes. Deterministic tests of a stochastic system only verify as much as the determinism covers.

Layer 2: Property tests

Some statements have to hold for every input, noise included. That’s what a property-testing library is for. The starter ships proptest. It generates inputs and, when a property fails, shrinks the failure down to a minimal counterexample:

proptest! {
    // A strictly closer and faster-closing situation never yields a
    // less severe decision.
    #[test]
    fn severity_is_monotone(base in track_report(), d in 1.0..50.0f64) {
        let closer = base.closer_by(d);
        prop_assert!(decide1(&closer) >= decide1(&base));
    }
}

Good properties for guardian: severity monotonicity, low-confidence tracks never causing Brake alone, a defined decision (no panic) for any report including NaN ranges, and an output present every cycle.

Layer 3: Statistical verdicts

The acceptance table says at least 99% of hard-brake scenarios end in Brake. That’s not a property of any single run; it’s a claim about a pass rate. Testing it by running 20 times and looking at the results gives you flaky CI and little confidence. The next page covers treating each run as a trial and testing the rate itself.

The table’s median-latency row needs a different analysis: retain every responder latency, report misses separately as response coverage, compute the median over responders as specified, and attach a bootstrap or documented distribution-free interval. A Bernoulli verdict may evaluate whether a run met a latency threshold, but that’s a different claim from the median row.

Layer 4: Mutation testing and proofs

Two stretch tasks for pairs with time left. Both come from Build Your Own Guardrails:

• Mutation-test the metrics. Run mutest-rs over the arbiter and metrics code. Each surviving mutant marks a claim your tests never check. Ask the agent to explain each survivor, then add a test that kills it or write down why it’s equivalent. A green suite is evidence only after this step.
• Build the protocol grid. The SPEC’s protocol alignment section has the four Euro NCAP CCRb cells and the sourced warn row. The sim gives you Scenario::Scripted; your agent builds the cells and the grid runner, and you review the unit conversions. One feotest verdict per cell, colour-graded, is the classroom version of the protocol’s per-point grading.
• Prove one invariant with Kani. Pick a property that must hold for every input, not only the sampled ones. “An empty report slice never yields Warn or Brake” is a good first choice. Ask the agent to write the #[kani::proof] for it. The result is stronger than a passing test: not “we found no failing input” but “no input of this shape exists”. Verus goes further when a contract deserves a full specification. Knowing that it exists is enough for today.