On trouve sur la page The ILTP Library - Benchmarking Theorem Provers for Intuitionistic Logic une liste de liens vers certains "prouveurs" pour la logique intuitionniste.

On cite encore les suivants :

 STRIP, écrit en C et conçu par Dominique Larchey-Wendling, Daniel Mery, et Didier Galmiche, tous trois chercheurs au Loria (Nancy).
 fCube, écrit en Prolog, concu par Mauro Ferrari, Camillo Fiorentini et Guido Fiorino.
 g5ip.pl, écrit en Prolog, par Frank Pfenning.
 LJT.pl, écrit en Prolog, par Roy Dyckhoff..
 CRIP.pl, article et texte d’un programme Prolog écrit par Roy Dyckhoff et Luis Pinto.
 Minlog, pour la logique minimale et la logique intuitionniste, écrit en C par John Slaney.
 Prouveur via S4, écrit en Ocaml avec une interface web, par Michel Levy .
 Déduction Naturelle, pour la logique propositionnelle intuitionniste et classique : une formule prouvée par le prouveur sans l’aide de la règle classique de la réduction à l’absurde (Raa) est une formule valide en logique intuitionniste. Il faut autoriser les fenêtres pop-up pour le site du prouveur pour voir la mention de l’usage des règles dans la preuve . Des informations plus complètes sur ce prouveur sont données pas Michel Lévy sur cette page.