The point that I was trying to make is that they have proven correctness within a specific abstraction, but the article incorrectly say the code is "hacker-proof". Hacking in most cases happens because we can break through abstractions.