Larch Prover

The Larch Prover, or LP for short, is an interactive theorem proving system for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s to reason about designs for circuits, concurrent algorithms, hardware, and software.

Unlike most theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP was intended to assist users in finding and correcting flaws in conjectures—the predominant activity in the early stages of the design process. It worked efficiently on large problems, had many important user amenities, and could be used by relatively naïve users.