LP, the Larch Prover LP, the Larch ProverLP is an interactive theorem proving system for multisorted first-order logic. It was developed by Stephen J. Garland and John V. Guttag at the MIT Laboratory for Computer Science (a predecessor of CSAIL, the MIT Computer Science and Artificial Intelligence Laboratory).
Unlike many theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP is intended to assist users in finding and correcting flaws in conjectures---the predominant activity in the early stages of the design process. LP works efficiently on large problems, has many important user amenities, and can be used by relatively naive users.
LP was used at MIT and elsewhere primarily during the 1990s to reason about designs for circuits, concurrent algorithms, hardware, and software. It was developed as part of the Larch project, which explored methods, languages, and tools for the practical use of formal specifications.
See LP's documentation for more information.
Executable verions of LP, as well as its source code, are available as indicated below. See the installation instructions for information on what you need to download and what to do with it.