K Framework

Spec sheet

Purpose

K is a rewrite-based executable semantic framework for defining programming languages, type systems, and formal analysis tools.Read 9 Oct 2026 · kframework.org

Support

The official site lists Discord as its most direct support channel and also links to a Matrix room.Read 9 Oct 2026 · kframework.org

Headquarters

The K site lists the address 202 S Broadway Ave #31, Urbana, IL.Read 8 Oct 2026 · kframework.org

Command line

The project README says K users should be comfortable with the command line and that GUI tools are not provided.Read 9 Oct 2026 · github.com

Concurrency

The site says K's rules make read and write access explicit, which supports defining concurrent languages with shared state.Read 9 Oct 2026 · kframework.org

Configurations and rules

K configurations organize program state into labeled, nestable cells, and rewrite rules describe how terms change.Read 9 Oct 2026 · kframework.org

Control flow

K represents computations as terms that can be matched, moved, modified, or deleted, supporting features such as exceptions and abrupt termination.Read 9 Oct 2026 · kframework.org

Core tools

The manual identifies kompile, kparse, krun, and kprove as its main user-facing tools.Read 8 Oct 2026 · kframework.org

Dependency requirement

K requires Z3 version 4.8.15; the installation page says other versions are unsupported and may cause incorrect behavior or performance issues.Read 8 Oct 2026 · github.com

Docker

The installation instructions provide Docker images with K pre-installed.Read 8 Oct 2026 · github.com

Documentation status

The K User Manual says it is still under construction and some features may have partial or missing documentation.Read 8 Oct 2026 · kframework.org

Editor integrations

The editor support page lists syntax support or plugins for Atom, BBEdit/TextWrangler, Emacs, IntelliJ IDEA, Notepad++, Pygments, Vim, and Visual Studio Code.Read 8 Oct 2026 · kframework.org

Editor support

The official site links to editor syntax highlighting support for popular editors and IDEs.Read 9 Oct 2026 · kframework.org

Execution and analysis

K’s command-line tools support compiling, running concrete or symbolic executions, and analyzing specifications through theorem proving.Read 8 Oct 2026 · kframework.org

Generated tools

A K language definition can provide tools such as a parser, interpreter, state-space explorer, and deductive program verifier.Read 9 Oct 2026 · kframework.org

Installation

The official site directs users to install K from GitHub releases and provides a `kup` installation command.Read 9 Oct 2026 · github.com

Known limitation

The FAQ says K does not provide explicit support for metamodel technologies such as EMF.Read 9 Oct 2026 · kframework.org

Maker and founding

Runtime Verification says it was founded in 2010 by Grigore Rosu, and that it released the K Framework in 2014.Read 8 Oct 2026 · runtimeverification.com

Python interface

pyk is K's scripting interface for Python and has API documentation.Read 9 Oct 2026 · kframework.org

Supported installation platforms

The installation page lists Ubuntu Jammy 22.04 and macOS Ventura 13 via Homebrew, and says K is not currently supported natively on Windows.Read 8 Oct 2026 · github.com

Supported systems

The installation guide lists Ubuntu 22.04, macOS via Homebrew, and Docker images; it says native Windows is not supported and recommends WSL 2.Read 9 Oct 2026 · github.com

Use cases

The official site links to projects using K, including examples and tools based on K definitions.Read 9 Oct 2026 · kframework.org

Where Specifiction places it

• Formal Verification Tools#22 of 347.5