# Automatic verification and interactive theorem proving

## TL;DR

This paper discusses the use of proof assistants and interactive theorem proving tools for automatic verification of correctness certificates in mathematics and computer science, enhancing reliability of proofs and software correctness.

## Contribution

It provides an overview of how interactive theorem proving systems facilitate the creation and automatic validation of formal correctness certificates.

## Key findings

- Proof assistants enable formal proof development.
- Automated validation ensures high confidence in correctness certificates.
- Applications span mathematics and software verification.

## Abstract

Automatic verification deals with the validation by means of computers of correctness certificates. The related tools, usually called proof assistants or interactive provers, provide an interactive environment for the creation of formal certificates whose correctness can be assessed in a purely automatic way. Such systems have applications both in mathematics, where certificates are proofs of theorems, and in computer science, where certificates testify the correctness of a given software with respect to its specification.