Les systèmes de vérification de faits s'appuient généralement sur des classificateurs à réseaux de neurones pour prédire la véracité, lesquels manquent de transparence explicative. Ce papier propose ProoFVer, un modèle basé sur une architecture seq2seq qui génère des inférences fondées sur la logique naturelle sous forme de preuves. Ces preuves consistent en des mutations lexicales entre des segments de l'énoncé et des éléments de preuve récupérés, chacune marquée par un opérateur de logique naturelle. La véracité d'un énoncé est déterminée exclusivement à partir de la séquence de ces opérateurs. Ainsi, ces preuves constituent des explications fidèles, ce qui rend ProoFVer fidèle par construction. Actuellement, ProoFVer obtient le meilleur taux d'exactitude des étiquettes et la deuxième meilleure note au classement FEVER. En outre, il améliore de 13,21 points de pourcentage le modèle suivant sur un jeu de données comprenant des instances contre-factuelles, démontrant ainsi sa robustesse. En tant qu'explications, les preuves présentent un meilleur chevauchement avec les raisonnements humains que les zones mises en évidence par l'attention, et elles aident les humains à prédire correctement les décisions du modèle plus souvent que l'utilisation directe des preuves.