The Abstract State Machines methodology offers a powerful, easy-to-use mechanism to formally specify the semantics of algorithms. The klar framework adds to it optimization capability, allowing the transformation of ASM specifications into efficient programs, which is important in order to use the specifications as realistic programs. Moreover, the optimizations are modules to be plugged-in “on the fly”, so that independent developers can develop their own optimizations without concerning about the internal details of the klar framework. Finally, the wide set of constructions of the language understood by the framework allows its use as a target for compilers aiming the ASM methodology.