Computer scientists can prove certain programs to be error-free with the same certainty that mathematicians prove theorems. By the time researchers began to understand the critical threats to computer security posed by the internet, program verification was ready for a comeback. This is easy enough to state in plain English. Translating the specification into formal language that a computer can apply is much harder — and accounts for a main challenge when writing any piece of software in this way.