Formal verification is described as the branch of computer science that formally establishes the correctness of systems. Generally, formal verification consists of suitably formalizing the system, followed by verifying it. In this talk, I shall describe two different ways how formal verification may contribute to other fields of computer science, beyond proving correctness.

Firstly, the process of formalization leads to interesting insights about the system, often ignored while designing the system. These insights may produce new, interesting ideas in designing more efficient systems, or theoretically proving properties about the system. As an example, I shall describe how formal verification of software transactional memories led to interesting notions like permissiveness, notions of correctness parametrized by relaxed memory models, and transactional prediction.

Secondly, I shall argue that the beautiful techniques at the core of efficient verification can also be exported to other fields. As an example, I shall show how to use abstraction-refinement techniques, commonly used to prove correctness of programs, to build efficient static schedulers for the cloud.