> "this program should not crash on any input" [...] though I expect those will be the last to be amenable to formal verification,

In the world of Rust, this is actually the easiest to achieve level of formal proofs.

Simple lints can eliminate panics and potentially-panicking operations (forcing you/LLM to use variants with runtime error handling, e.g. `s[i]` can become `s.get(i).unwrap_or(MyError::RuhRoh)?`, or more purpose-specific handling; same thing for e.g. enforcing that arithmetic never underflows/overflows).

Kani symbolically evaluates simple Rust functions and ensures that the function does not panic on any possible value on it's input, and on top of that you can add invariants to be enforced (e.g. search for an item in an array always returns either None or a valid index, and the value at that index fulfills the search criteria).

(The real challenge with e.g. Kani is structuring a codebase such that it has those simple-enough subparts where formal methods are feasible.)