LETOS -- A Lightweight Execution Tool for Operational Semantics A lightweight tool is proposed to aid in the development of operational semantics. To use letos, an operational semantics must be expressed in its meta-language, which itself is a superset of Miranda. The letos compiler is smaller than comparable tools, yet letos is powerful enough to support publication quality rendering using LaTeX, fast enough to provide competitive execution and tracing using Miranda or Haskell, and versatile enough to support derivation tree browsing using Netscape. Letos has been applied to a Java Secure Processor, which is a version of the Java Virtual Machine intended to run on smart cards. Letos has also been used with subsets of various programming languages. Letos is unique in that it helps to check that a specification is operationally conservative.