Grigore Rosu's research group has added a powerful tool with a deceptively simple name to the arsenals of people trying to write secure smart contracts. The K Framework, developed over the last decade in Rosu’s Formal Systems Laboratory (FSL) in collaboration with his U of I-licensed startup Runtime Verification (RV), significantly eases the development of formal semantics of programming languages.