Exactly! (Except formal methods are not one but many methods and tools that are as different from one another as code review is from testing. Also, I wouldn't call TLA+ a "lightweight" formal method despite being relatively easy to learn and to apply; it's hard to get more heavyweight than TLA+.)
While we’re on the subject, I think it’s worthwhile to explain the name “formal methods”, and especially “formal” (methods just means techniques, in our case techniques for software verification), as I’ve seen people constantly misuse it.
Formal means mechanical, i.e. doable in principle by a computer (sometimes we say doable or checkable by a computer, but the two are equivalent from a computability perspective though not from a complexity perspective). So when you say you have a formal proof that does not mean you have a mathematical proof, but a proof that can be verified by a computer. Then why do we say "formal" instead of "mechanical"? Because the word formal was used for centuries before Alan Turing discovered that it is equivalent to "mechanical." The main idea of symbolic logic is that of the formula, or logical form; a sentence whose truth can be derived by the direct manipulation of its form (syntax) without any use of intuition or understanding. So, to this day, when we talk of things making use of symbolic (or formal) logic, we say formal rather than mechanical.
Now, if formal means mechanical and methods means techniques for software verification, are testing and type checking — both software verification techniques that are carried out by the computer — formal methods? Technically they are! But formal methods is also the name of an academic discipline, and so formal methods usually refers to whatever it is that people who research formal methods study, and type checking have not traditionally been a part of that discipline. What’s interesting that both of them — or, rather, certain forms of them — are now actually part of formal methods research. A few formal methods researchers study dependent type systems, type systems that can express a far richer set of program properties than simple type systems, and the study of concolic testing, a combination of symbolic and abstract interpretation/model-checking and concrete (i.e. “normal”) testing is a very hot topic in formal methods research at the moment. What's common to all topics in formal methods research is some use of formal logic.
While we’re on the subject, I think it’s worthwhile to explain the name “formal methods”, and especially “formal” (methods just means techniques, in our case techniques for software verification), as I’ve seen people constantly misuse it.
Formal means mechanical, i.e. doable in principle by a computer (sometimes we say doable or checkable by a computer, but the two are equivalent from a computability perspective though not from a complexity perspective). So when you say you have a formal proof that does not mean you have a mathematical proof, but a proof that can be verified by a computer. Then why do we say "formal" instead of "mechanical"? Because the word formal was used for centuries before Alan Turing discovered that it is equivalent to "mechanical." The main idea of symbolic logic is that of the formula, or logical form; a sentence whose truth can be derived by the direct manipulation of its form (syntax) without any use of intuition or understanding. So, to this day, when we talk of things making use of symbolic (or formal) logic, we say formal rather than mechanical.
Now, if formal means mechanical and methods means techniques for software verification, are testing and type checking — both software verification techniques that are carried out by the computer — formal methods? Technically they are! But formal methods is also the name of an academic discipline, and so formal methods usually refers to whatever it is that people who research formal methods study, and type checking have not traditionally been a part of that discipline. What’s interesting that both of them — or, rather, certain forms of them — are now actually part of formal methods research. A few formal methods researchers study dependent type systems, type systems that can express a far richer set of program properties than simple type systems, and the study of concolic testing, a combination of symbolic and abstract interpretation/model-checking and concrete (i.e. “normal”) testing is a very hot topic in formal methods research at the moment. What's common to all topics in formal methods research is some use of formal logic.