Design and implement your programming language and software analysis tools with mathematical rigor. Formally verify your programs for maximum assurance.

K gives you
  • a framework for defining formal syntax & semantics of programming languages
  • a suite of execution and analysis tools parametric in your programming language
  • a program verifier whose trust base is your programming language formal semantics

Latest from the K Blog:

May 25 2018 K Framework – An Overview by Grigore Rosu
Feb 06 2018 K Framework Enables Verification of Smart Contracts by Mike Koon
Dec 15 2017 IELE: A New Virtual Machine for the Blockchain by Grigore Rosu
Dec 14 2017 RV Inc. & FSL @ UIUC Release First Formal Viper Tools by Philip Daian
Dec 06 2017 ERC20-K: Formal Executable Specification of ERC20 by Grigore Rosu

Based on cutting edge research, K allows you to define domain-specific or general-purpose programming languages, and then generate powerful, rigorous, and automatic tools for formally analyzing programs in those languages. No resources wasted anymore to design and implement languages and tools in an adhoc way.