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
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.
In the video below we demonstrate use of the K Lab tool, which helps users interactively explore and debug proofs generated by the K prover.