My own work on formal methods centered around parallel computation. Ray Miller, Shmuel Winograd and I did work that foreshadowed the theory of systolic algorithms. Miller and I introduced the parallel program schema as a model of asynchrononous parallel computation; in the course of this work we introduced vector addition systems and initiated the study of related decision problems. The most notorious of these was the reachability problem, which after many false tries was proved to be decidable through the efforts of several researchers, culminating in a 1982 paper by Rao Kosaraju.
A related post: Ray Miller's memoirs.