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.
For a general introduction to LP, see the following topics.