What is the difference between formal methods and formal verification?
Looked at their corresponding pages on wikipedia:
It said formal verification uses formal methods.
Is it that formal verification uses software whereas formal methods is theoretical?
What I understood was that formal verification uses a formal model of a system and checks if that model adheres to a formally defined specification.
But could not figure out what the difference between that and formal methods is.
The short answer is: formal methods is a collection of mathematical tools that enable us to reason about the correctness of systems. Formal verification is one (major) application of these tools to check whether a given program is correct.
Both formal verification and formal methods have practical and theoretical sides, that's not really the difference.
There is one-sided containment here: everything that falls under formal verification is also a part of formal methods. To understand the difference, we need to see something that is considered formal methods, but not formal verificaiton.
A prominent example of this is automated synthesis: here, we are given a reactive specification, i.e., a formula $\psi$ over input and output signals, that tells us which input/output sequences are ``good''. Then, the goal is to automatically generate a reactive system (transducer) that for each input sequence generates an output sequence such that the resulting computation is correct.
Synthesis is not verification, since there is nothing to verify: you are not checking the correctness of anything, but automatically constructing a correct system given only a specification.
Technically, the classical "formal methods" used for synthesis are typically games (or sometimes tree automata).
I think synthesis is perhaps the most clear example of the difference, but I'm sure there are other examples that can be considered formal methods but not formal verification.
