Not sure I follow the analogy, so apologies if I'm reading it backwards, but we do in fact have standards for "good enough" brakes without being brake-maxxers.

Similarly here, I'd argue that a verified implementation with correctness proofs, mechanical translation, and easily auditable theorems seems close to good enough? A lot rides on the Claude-built translator, I suppose, but the trusted code for that project seems to be tiny in comparison to what it would have been 2 years ago!