Formaalne tõestus on sõnaliste või matemaatiliste väidete jada, mida kasutatakse antud järelduse loogilise vajalikkuse demonstreerimiseks. Sellised tõestused nõuavad ranget ja täpset keelekasutust, kuna keeleline mitmetähenduslikkus võib tõestuse kergesti mõttetuks muuta. Paljudel juhtudel võib selle probleemi vältimiseks esitada formaalse tõestuse sümboolselt või matemaatiliselt, et vältida keele tekitatavat segadust nii palju kui võimalik. Sellised rangelt formaalsed tõestused algavad tavaliselt ühest või mitmest väljakujunenud või teoreetilisest eeldusest. Neile eeldustele järgnevad aksioomid või väited, mis tulenevad loogiliselt premisside eelnevatest väidetest ja lõpevad lõpliku järeldusega või tõestatud teoreemiga, mis sarnaselt eelnevatele väidetele on esialgsete eelduste ja aksioomide loogiliselt vajalik tulemus.
Erinevalt formaalsest tõestusest tugineb enamik argumente igapäevaelus üldkeelele ega ole üldiselt loogiliselt range. Need ei pruugi näiteks pärineda hästi ehitatud ruumide kogumist või võivad tugineda retoorilistele üleskutsetele – emotsioonidele või autoriteedile –, millel pole kohta ametlikus tõendis. Kuigi formaalne tõestus on väärtuslik tänu oma võimele näidata väite õigsust eelduste kogumi põhjal, on oluline meeles pidada, et formaalsetest tõestustest on vähe või üldse mitte mingit kasu, kui arutletakse millegi üle, mida ei saa loogika vallas lõplikult tõestada. . Samuti kehtivad need ainult algsete eelduste kontekstis ega näita seetõttu universaalseid tõdesid.
Enamik formaalseid tõestusi põhinevad “formaalsel keelel”, mis koosneb kas normaalse keele alamhulgast või sümbolitest. Näiteks matemaatiline formaalne tõestus väljendub matemaatikas kasutatavate sümbolite abil ega tugine üldse verbaalsele keelele. Paljudel juhtudel asendatakse sõnad sümbolitega, nii et isegi mittematemaatilist formaalset tõestust saab lihtsa sümboolse loogika kujul mõista ilma potentsiaalselt mitmetähenduslikke sõnu kasutamata.
Paljud erinevad valdkonnad, tavaliselt akadeemilises ringkonnas, kasutavad ametlikke tõestusi. Kõige ilmsem näide on matemaatika, valdkond, mis põhineb suuresti tõestuste kasutamisel. Samamoodi tugineb arvutiteadus rangete formaalsete loogiliste edenemise kasutamisele, et tagada arvutitele absoluutselt täpsete juhiste andmine. Filosoofia, eriti analüütiline filosoofia, tugineb ka formaalsete tõendite kasutamisele, et demonstreerida erinevate filosoofiliste väidete õigsust erinevate varem väljakujunenud või teoreetiliste eelduste kontekstis.