The Formal Systems Laboratory (FSL) at the University of Illinois at Urbana-Champaign (UIUC) is a group of researchers and developers aiming to increase the quality of computing systems. We achieve this goal by developing tools and ideas that allow us to precisely determine how software behaves and to verify that software behaves correctly. One such tool is the K framework, a system for easily creating new programming languages and formally defining existing ones. Programs written in a language created or defined in the K framework can be reasoned about rigorously and can be used more confidently in safety-critical systems.