The Larch Prover, or LP for short, is a tool that helps prove mathematical statements in a type of logical system called multi-sorted first-order logic. It was used at MIT and other places during the 1990s to check and improve designs for circuits, concurrent algorithms, hardware, and software.

Unlike most theorem provers, which try to automatically find proofs for correct statements, LP was designed to help users find and fix problems in their ideas during the early stages of creating designs. It worked well on big problems, had features that made it easier to use, and could be operated by people who were new to using such tools.

Development

LP was created by Stephen Garland and John Guttag at the MIT Laboratory for Computer Science, with help from James Horning and James Saxe at the DEC Systems Research Center. It was part of the Larch project, which focused on creating precise rules for describing systems. LP was based on the REVE 2 system, which was developed by Pierre Lescanne and Randy Forgaard, with assistance from David Detlefs and Katherine Yelick. LP supports different types of proofs, including those using equations with special rules, cases, contradiction, induction, generalization, and specialization. LP was written in the CLU programming language.