Like Ada or Ocaml or Haskell or something.
Or even require like MC / DC testing or MISRA C verification.
Or even some of the languages that apply Hoare checks, like Ada SPARK or FRAMA-C or VALE or whatever.
I don't have the budget to test how that would work but it seems interesting.