proof assistant author
- HOL John Harrison, Konrad Slind, Rob Arthan
- Mizar Andrzej Trybulec
- PVS Bart Jacobs, John Rushby
- Coq Laurent Thery, Pierre Letouzey, Georges Gonthier
- Otter/Ivy Michael Beeson, William McCune
- Isabelle/Isar Markus Wenzel, Larry Paulson
- Alfa/Agda Thierry Coquand
- ACL2 Ruben Gamboa
- PhoX Christophe Raffalli, Paul Roziµere
- IMPS William Farmer
- Metamath Norman Megill
- Theorema Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
- Lego Conor McBride
- Nuprl Paul Jackson
- mega Christoph BenzmÄuller, Armin Fiedler, Andreas Meier, Martin Pollet, JÄorg Siekmann
- B method Dominique Cansell
- Minlog Helmut Schwichtenberg