In a previous blog post, we talked about formal verification and how we can convince ourselves (and others!) that a piece of software really works as intended. Now that we have managed to complete formal verification of our first component, the keystore, I would like to talk about it in more detail.