Em lógica, uma derivação formal (ou prova formal) é uma sequência finita de sentenças onde cada sentença pode ser um axioma ou então pode ser obtida como consequência direta de sentenças anteriores na sequência utilizando-se uma regra de inferência. A última sentença na sequência é um teorema do sistema formal. A noção de teorema não é em geral efetiva, pois pode não haver um método através do qual nós possamos sempre encontrar uma derivação de uma dada sentença ou determinar que não existe nenhuma derivação. O conceito de dedução é uma generalização do conceito de derivação.