Formal proof
The activity of formal proof is necessarily part of the activity of formal validation, which consists in providing assurance of the validity of a theorem. Validation can implement different techniques, the two main ones being formal proof and model checking.
PRESENTATION
The “Formal Proof” consists in proving theorems with the help of a proof assistant. These tools allow, for some, to automatically execute parts (or even the entirety) of a proof, but above all to validate the entirety of the proof made by the user so that a theorem is not proved in an erroneous way. A proof assistant is a tool with a theorem description language and a proof description language (which may or may not be the same).
There are a number of proof assistants that have been developed and are used either in the academic world or in industry. They can implement various techniques (See Formal Methods on Wikipédia).
The specificity of the formal method B is that the lemmas to be proved are produced by a tool (proof obligation generator) in a language corresponding to the first order logic associated with set theory.
The proof tools used in the framework of the method include:
1- A base of inference rules associated with an engine containing heuristics
2- A SAT-type prover
DIFFERENT INTERFACES HAVE BEEN DEVELOPED TO ASSIST IN WRITING THE EVIDENCE:
1- Atelier B
2- ProB
3-Rodin plaftorm prover (update site: https://www.atelierb.eu/update_site/atelierb_provers)
| Plug-in name | Version | Status | MCV | Release Date |
| Atelier-B provers | 2.3.0 | Available | 3.3.0 | 02 Dec 2020 |