Surasak Phetmanee

Before a planetary rover drives the arc its planner picked, our checker computes the exact probability that the arc ends stuck or crashed within the next eight range bands, for every candidate arc, on the rover's own computer. Mars is 4 to 24 light minutes away, so nothing can be checked on Earth in the loop, and the flight computer is far slower than a laptop. Pipeline: a Curiosity Navcam frame (NASA AI4Mars) → Meta SAM 2.1 image encoder features plus a linear probe classify the terrain → the frame becomes a stochastic grid (slip, sink, collision) → a C model checker with no dependencies evaluates all 27 candidate arcs → veto or rerank the planner's choice. Trust comes from checking the checker: it agrees with the PRISM probabilistic model checker on 780 property checks (MDPs and stochastic games) and on 5,084 terrain values, and every map up to 3×3 (1,985,305 maps) passes under AddressSanitizer and UBSan. All 27 arcs of a scene are checked in about 95 µs on an efficiency core standing in for a flight CPU. Findings on 20 held out scenes: the checker finds a strictly safer arc than the planner in 9 of 20 scenes, but the gain is small; almost every veto means "stop", not "go elsewhere"; and the perception model changes the verdict more than the arc choice does (vetoes drop from 13 to 6 when SAM 2 replaces human labels). Terrain slip and sink probabilities are assumed and labelled as such.