K Framework

A rewriting-logic-based framework for defining the formal semantics of programming languages (Roșu et al., University of Illinois at Urbana-Champaign, 2003–). Language semantics written in K are simultaneously: (1) an executable interpreter, (2) a symbolic executor, (3) a target for model-checking, and (4) a target for deductive verification — all derived from a single specification.

K has been used to formalise C (KCC), Java, JavaScript, LLVM, Ethereum (see KEVM), and others. It realises what the formal-methods community calls “one semantics, many tools”: the same definition powers interpretation, verification, and analysis without re-implementation.

Tags

#formal-semantics #rewriting-logic #verification

KEVM

An executable formal semantics of the Ethereum Virtual Machine, written in the K Framework (Runtime Verification, Inc., 2017–). Unlike the Ethereum yellow paper (prose + informal pseudo-mathematics), KEVM is a machine-checkable specification: you can run a contract against KEVM and get the same result the semantics prescribes, byte-for-byte.

Its value is twofold. (1) Reference semantics — disputes about “what does this opcode do?” can be resolved by running KEVM, not by re-reading English prose. (2) Verification target — contracts can be proved correct against KEVM using the K framework’s symbolic execution and theorem-proving tools, rather than against an ad-hoc test suite.

House on Rock - LangSec in Ethereum Classic holds up KEVM as the remediation Ethereum Classic should adopt: replace the yellow paper with an executable semantics and give verification tools a standard target.

K Framework

Tags

Backlinks