Preuve formelle assistée par ordinateur (LMFI)

HOL

Symmetry in HOL

Isabelle

Isabelle (named by Lawrence Paulson after the daughter of Gérard Huet, as a tribute): a popular generic theorem prover