Métodos formais são o uso de modelagem matemática para a especificação, desenvolvimento e verificação de sistemas em ambos software e eletrônico hardware<. Os métodos formais são usados para garantir que esses sistemas sejam desenvolvidos sem erros.
A base matemática subjacente aos métodos formais é usada para ajudar a garantir a adequação do projeto para resultar em funcionalidade, consistência e confiabilidade no mundo real do produto final.
Tal como em outros campos da engenharia, os métodos formais aplicam a matemática à engenharia de software e hardware, a fim de adicionar certeza ao projeto e teste desses sistemas. Os métodos formais são usados para descrever as funções de um sistema antes do design com linguagens descritivas garantindo a funcionalidade do sistema. Métodos formais podem ser usados no desenvolvimento dependendo do rigor com que o sistema é descrito. As especificações formais podem funcionar como um guia para os requisitos. Em análise, os métodos formais fornecem a descrição das funções através das quais o programa pode ser verificado.
A extensão em que os métodos formais são implementados pode variar. Algumas vezes, a implementação completa de métodos formais é considerada muito cara, exceto no caso de sistemas criticamente importantes e projetos complexos onde erros podem resultar em redesigns ou refabricação dispendiosos. Muitas vezes, os métodos formais são usados apenas para descrever a função desejada e para orientar o desenvolvimento. Isto é considerado nível 0 ou métodos formais lite. When formal methods are additionally used to verify functions, it is considered level 1. Level 2, the highest degree of formal methods, is when the full system is machine verified through all its functions.
Some examples of systems that might be fully specified under formal methods would be complex semi-conductors such as CPUs or GPUs or critical systems in software like that which is used in SCADA for control of power plants