There is a subset of Ada called SPARK that is intended to allow for at least some degree of automated formal verification. Which is not quite the same as automa

There is a subset of Ada called SPARK that is intended to allow for at least some degree of automated formal verification. Which is not quite the same as automated error detection, but I would assume if your code passes the verification, the chance of bugs hiding in it is pretty much nil (assuming, of course, the verifier is not buggy itself).