Muodollinen todiste on sanallisten tai matemaattisten lausuntojen sarja, jota käytetään osoittamaan tietyn johtopäätöksen looginen välttämättömyys. Tällaiset todisteet edellyttävät tiukkaa ja täsmällistä kielenkäyttöä, koska kielellinen epäselvyys voi helposti tehdä todistuksen merkityksettömäksi. Monissa tapauksissa tämän ongelman välttämiseksi voidaan esittää muodollinen todiste symbolisesti tai matemaattisesti kielen aiheuttaman sekaannuksen välttämiseksi mahdollisimman paljon. Tällaiset tiukasti muodolliset todisteet alkavat yleensä yhdellä tai useammalla vakiintuneella tai teoreettisella oletuksella. Näiden lähtökohtien perässä on aksioomeja tai lausuntoja, jotka seuraavat loogisesti tilojen aiemmista lausunnoista ja päättyvät lopulliseen johtopäätökseen tai todistettuun lauseeseen, joka edellisten lausuntojen tavoin on loogisesti välttämätön tulos alkuperäisistä premisioista ja aksioomeista.
Päinvastoin kuin muodollinen todiste, useimmat argumentaatiot päivittäisessä elämässä perustuvat yhteiseen kieleen eivätkä yleensä ole loogisesti tiukkoja. Ne eivät esimerkiksi ole peräisin hyvin rakennetuista tiloista tai ne voivat vedota retorisiin vetoomuksiin-tunteiden tai auktoriteetin suhteen-joilla ei ole sijaa muodollisessa todistuksessa. Vaikka muodollinen todiste on arvokas, koska se kykenee osoittamaan väitteen paikkansapitävyyden premissien perusteella, on tärkeää muistaa, että muodollisista todisteista on vähän tai ei lainkaan hyötyä, kun keskustellaan kaikesta, mitä ei voida osoittaa lopullisesti logiikan alalla . Lisäksi niitä sovelletaan vain alkuperäisten lähtökohtien puitteissa, eivätkä ne siksi esitä yleismaailmallisia totuuksia.
Useimmat muodolliset todisteet perustuvat ”viralliseen kieleen”, joka koostuu joko normaalikielen osajoukosta tai symboleista. Esimerkiksi matemaattinen muodollinen todiste ilmaistaan käyttämällä matematiikassa käytettyjä symboleja, eikä se perustu lainkaan sanalliseen kieleen. Monissa tapauksissa sanat korvataan symboleilla siten, että jopa ei-matemaattinen muodollinen todiste voidaan ymmärtää yksinkertaisen symbolisen logiikan muodossa käyttämättä mahdollisesti epäselviä sanoja.
Monet eri alat, yleensä akateemisessa maailmassa, käyttävät muodollisia todisteita. Ilmeisin esimerkki on matematiikka, ala, joka perustuu suurelta osin todisteiden käyttöön. Samoin tietotekniikka perustuu tiukkojen, muodollisten loogisten edistysaskeleiden käyttöön, jotta tietokoneille annetaan ehdottoman tarkat ohjeet. Filosofia, erityisesti analyyttinen filosofia, perustuu myös muodollisten todisteiden käyttämiseen erilaisten filosofisten väitteiden paikkansapitävyyden osoittamiseksi eri aikaisemmin vahvistettujen tai teoreettisten lähtökohtien yhteydessä.