We begin by describing the Larch approach to specification and illustrating it with a few small examples. We then discuss LP, the Larch proof assistant, a tool that supports all the Larch languages. Our intent is to give you only a taste of these things. For a comprehensive look at Larch see John V. Guttag and James J. Horning (editors), with Stephen J. Garland, Kevin D. Jones, Andres Modet, and Jeannette M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993.