A formal proof activity is generally part of the formal validation activity, which consists in ensuring the validity of a theorem. Validation may be based on a number of techniques, the two main ones being formal proof and model checking.

## FORMAL PROOF PRESENTATION

**Formal proof** consists in demonstrating theorems with a proof assistant. Some of these tools allow for the automatic execution of portions (even the entirety) of a proof, but are most often used to validate proof established by the user so that a theorem is not proven in error.

A proof assistant is a tool with which a theorem description language and proof description language (which can be identical) are associated.

A certain number of proof assistants have been developed and are used within academia and industry. They can use a variety of techniques (see Formal Method on Wikipedia).

The particularity of B Method is that the lemmas that must be proven are produced by a tool (a proof obligation generator) in a language that corresponds to the first order logic associated with the set theory.

**The proof tools used in the context of the method include:**

**>** An inference rules database associated with a motor that includes heuristics**>** A SAT-type prover

**Different interfaces have been developed to help with proof writing:**

**>** Atelier B**>** ProB**> **Rodin platform prover

Plug-in name | Version | Status | MCV | Release date |

Atelier-B provers | 2.3.0 | Available | 3.3.0 | 02 Dec 2020 |