[irundebian]

It's possible. You can prove absence of runtime errors with Ada/SPARK (which is using theorem provers).