Projects using K



  • 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.

  • 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.

  • 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.

  • KEVM (Sep 2017 - Present)

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

  • 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.

  • Boogie (Apr 2020 - Present)

    Presents an executable formal semantics for Boogie, an intermediate language for verification. The K semantics of Boogie provides an independent verification engine for programs compiled to Boogie. This, for example, allows Dafny users to either discharge their verification goals using Boogie or using the K semantics of Boogie.

  • Elrond (July 2020 - Present)

    The semantics of Elrond is a wrapper around KWasm which extends it with the Elrond blockchain primitives. This extension enables developers targeting the Elrond blockchain to measure coverage of their test-suite directly at the Wasm level.

Archived