I metodi formali sono l'uso della modellazione matematica per la specifica, lo sviluppo e la verifica dei sistemi in entrambi Software ed elettronica hardware. I metodi formali vengono utilizzati per garantire che questi sistemi siano sviluppati senza errori.
Le basi matematiche alla base dei metodi formali vengono utilizzate per garantire l'adeguatezza del progetto per ottenere funzionalità, coerenza e affidabilità nel mondo reale nel prodotto finale.
Proprio come in altri campi dell'ingegneria, i metodi formali applicano la matematica all'ingegneria del software e dell'hardware al fine di aggiungere certezza alla progettazione e al collaudo di questi sistemi. I metodi formali vengono utilizzati per descrivere le funzioni di un sistema prima della progettazione con linguaggi descrittivi che garantiscono la funzionalità del sistema. I metodi formali possono essere utilizzati nello sviluppo a seconda del rigore con cui viene descritto il sistema. Le specifiche formali possono fungere da guida ai requisiti. In analisi, i metodi formali forniscono la descrizione delle funzioni mediante le quali il programma può essere verificato.
La misura in cui vengono implementati i metodi formali può variare. A volte, la piena implementazione di metodi formali è considerata troppo costosa, tranne nel caso di sistemi di importanza critica e progetti complessi in cui gli errori possono comportare costose riprogettazioni o rifabbricazioni. Spesso i metodi formali vengono utilizzati solo per descrivere la funzione desiderata e per guidare lo sviluppo. Questo è considerato livello 0 o metodi formali lite. Quando i metodi formali lo sono inoltre utilizzato per verificare le funzioni, è considerato livello 1. Il livello 2, il più alto grado di metodi formali, è quando l'intero sistema è verificato dalla macchina attraverso tutte le sue funzioni.
Alcuni esempi di sistemi che potrebbero essere completamente specificati con metodi formali sarebbero complessi semiconduttori ad esempio CPU or GPU o sistemi critici nel software come quello utilizzato in SCADA per il controllo delle centrali elettriche