> formal semantics for both C and Rust in Lean, both sound like Herculean efforts

If we're doing Ancient Athens, then Platonic Methexis probably fits better.