github.com/kframework/kore ↗

About kframework/kore

Kore is the symbolic execution engine that powers the K Framework, a term rewriting-based specification language. This project implements tools for symbolically executing programs written in languages specified using K by operating on Kore, an intermediate representation produced when K compiles language specifications. The core component is kore-rpc-booster, a JSON RPC-based server that implements symbolic term rewriting according to the KORE RPC protocol, allowing external tools to request execution and simplification of Kore terms against a language definition.

The project is intentionally low-level and not designed for direct end-user interaction. Instead, it serves as a backend for higher-level tools like pyk, a Python-based theorem prover in the K Framework repository that builds on top of the KORE RPC protocol. The engine can optionally use a dynamic library compiled by the LLVM backend to optimize simplification of boolean-sorted terms, integrating with the broader K compilation pipeline.

Development is managed through both Stack and Cabal, with extensive support for Nix-based development environments and continuous integration. The project includes integration testing infrastructure that compiles the K Framework against the current Haskell backend version, performance testing scripts for downstream projects like KEVM and Kontrol, and tooling for analyzing test failures and generating reproducible test cases from bug reports. The codebase is written in Haskell and requires strict formatting compliance via Fourmolu.