Kripke is a countermodel checker for intuitionistic propositional logic. Kripke takes in a Kripke-tree and a sequent of propositional formulas and decides whether the Kripke-tree is a countermodel to the sequent, i.e., whether its root forces all assumptions of the sequent but not the conclusion. As another option it annotates the nodes of the tree with all forced subformulas of formulas that appear in the sequent. A third option finds a maximal node that forces all assumptions of the sequent but not the conclusion, if such a node exists. Finally, there is an option that lists all maximal nodes of that kind.
Kripke is written in Standard ML, and is intended to be compiled using MLton, producing an executable, which can be exectuted from the shell.
Kripke is described in the paper Kripke: a Countermodel Checker for Intuitionistic Propositional Logic.
Kripke's source consists of a single file, kripke.sml.