Projects using K

A list of projects using the K framework. If you are working on something interesting, and you want to share it with the community, let us know on our socials, and we will feature you on this list.



  • KAVM (Feb 2022 - Present)

    The Algorand Virtual Machine and TEAL Semantics in K
    KAVM leverages the K Framework to empower Algorand smart contracts' developers with property-based testing and formal verification.

  • KPlutus (2016 - Present)

    The K Semantics of Plutus-Core

  • Dedukti (Mar 2021 - Present)

    This project aims to translate real K semantics into Dedukti.

  • KWasm (Aug 2015 - Present)

    KWasm is the K semantics of WebAssembly. WebAssembly is a low-level (but simple and streamlined) assembly language that was originally developed to provide a fast execution engine for browser-based tools. More recently, it has been used in several blockchain smart-contract platforms as the underlying language for executing financial agreements. KWasm has been used for measuring coverage of test-suites over Wasm code and verifying programs which are compiled to Wasm.

  • KEVM (Sep 2017 - Present)

    KEVM is the K semantics of the Ethereum Virtual Machine. It passes all the Ethereum Test Suite, and is used for verifying EVM programs.

  • IELE (Oct 2016 - Present)

    IELE is the underlying VM integrated into the Cardano blockchain. IELE is a register-based VM (inspired by LLVM), which attempts to avoid many of the missteps in design present in EVM.

  • K-Michelson (Oct 2019 - Present)

    K-Michelson is the K semantics of Michelson blockchain programming language, which powers the Tezos blockchain. KMichelson provides additional testing tools for developers, including a unit-testing framework which is extendable to symbolic property testing.

  • C (Jul 2010 - Present)

    The K semantics of the C programming language specifies the translation, linking, and execution semantics of the C language according to the official C standard. It has been used to build tools like RV-Match, which detects undefined behaviors in users programs by running their test-suites through the C semantics.

Archived