Comment by ahelwer

Worth noting formally verified programs are unhackable to the extent three things hold true:

1) Your model of the world corresponds to the world in which the program runs - for example, hardware is usually assumed to be bug-free.

2) The properties you've proven the program to hold are sufficient to stop the hacker from accomplishing their goals.

3) No bugs exist in your theorem prover.