"Formal methods" means the mathematics and modeling applicable to the specification, design, and verification of software. The emphasis is on the creation of theories and tools to aid these activities. The methods are "formal" in the sense that they are precise enough to be implemented on a computer. With these techniques, we can develop specifications and models which describe all or part of a system's behavior at various levels of abstraction, and use them as input to an automated theorem prover. For requirements engineering, the input may be a collection of partial specifications, and the output may be a report on where inconsistencies lie. For design, the input may be a specification and a design step, and the output is either "Yes, the design step is consistent with the specification.", or "No, and here's why not: ... ". For verification, the input may be a specification and a desired property of system behavior, and the output may be either "Yes, the property is a consequence of the specification.", or "No, and here's why not: ... ".

Although a complete formal verification of a large complex system is impractical at this time, formal methods are applied to various aspects, or properties, of large systems. More commonly, they are applied to the detailed specification, design, and verification of critical parts of large systems such as avionics and aerospace systems, and to small, safety-critical systems such as heart monitors.