I've rarely seen what you're describing although I know plenty work remains go be done. So, could you give examples of code injections or mission-ending errors at code level that Haskell toolchains or Isabelle/HOL couldnt handle?