Skip to content
@runtimeverification

Runtime Verification Inc.

runtime verification logo

Runtime Verification specializes in formal verification of software systems, providing the highest level of assurance for the correctness and security of smart contracts and other critical software. Our mission is to deliver open-source formal verification and developer tooling to reduce the costs of auditing and enable continuous formal verification and testing on each commit.

Schedule a call with us to discuss formal verification & security engagements, along with custom tooling development & integrations.

Since 2018, we have provided formal verification and security services to numerous blockchain foundations and dApps, such as EigenLayer, Optimism, Uniswap, Ethereum Foundation, Lido, Gnosis, Morpho, Polkadot and many others.

Here you can find a complete list of our previous engagements.

This GitHub Organization hosts all of Runtime Verification's open-source tools and projects, designed to improve the security and reliability of blockchain and software systems through formal verification.

We are currently building and maintaining the following projects:

  1. K Framework: A rewrite-based executable semantic framework that allows formal definition of programming languages and VMs.
  2. Kontrol: Combines KEVM and Foundry to enable developers to perform formal verification without learning new languages or tools.
  3. Simbolik: VSCode-compatible Solidity debugger with built-in symbolic execution engine designed to assist in debugging and verifying smart contracts.
  4. KEVM: An executable formal specification of the Ethereum Virtual Machine (EVM) in the K framework.
  5. KWasm: A formal semantics of WebAssembly in the K framework, allowing formal analysis and verification of WebAssembly programs.
  6. KMIR: A formal semantics of the Rust MIR (Mid-level Intermediate Representation) in the K framework.
  7. Kasmer: A formal verification tool for WebAssembly, based on KWasm.
  8. KaaS: CI Integrated Cloud-Based Symbolic Execution.

You can learn more about our tools from Runtime Verification docs.

We invite developers, researchers, and enthusiasts to explore and contribute to our projects, as we continue to push the boundaries of formal verification and secure software development.

Pinned Loading

  1. k Public

    K Framework Tools 7.0

    Python 472 153

  2. evm-semantics Public

    K Semantics of the Ethereum Virtual Machine (EVM)

    Python 518 151

  3. kontrol-demo Public

    Foundry blog posts' executable demos

    Solidity 12 4

  4. imp-semantics Public

    The K semantics of IMP and associated tools

    Python 4 1

  5. kontrol Public

    Python 65 10

  6. mir-semantics Public

    Python 15 3

Repositories

Showing 10 of 176 repositories
  • mir-semantics Public
    Python 15 3 6 2 Updated Feb 28, 2025
  • haskell-backend Public

    The symbolic execution engine powering the K Framework

    Haskell 215 BSD-3-Clause 44 136 17 Updated Feb 27, 2025
  • evm-semantics Public

    K Semantics of the Ethereum Virtual Machine (EVM)

    Python 518 BSD-3-Clause 151 68 13 Updated Feb 27, 2025
  • komet Public
    WebAssembly 0 BSD-3-Clause 1 2 2 Updated Feb 27, 2025
  • evm-equivalence Public

    Equivalence proofs of EVM models

    Lean 0 0 0 0 Updated Feb 26, 2025
  • _audits_lidofinance_dual-governance_fork Public Forked from lidofinance/dual-governance

    Lido Dual Governance contracts

    Solidity 1 MIT 9 5 9 Updated Feb 26, 2025
  • stable-mir-json Public

    KMIR Rust Library

    Rust 2 0 13 2 Updated Feb 26, 2025
  • publications Public

    Publications of Runtime Verification, Inc.

    HTML 88 20 0 0 Updated Feb 26, 2025
  • k Public

    K Framework Tools 7.0

    Python 472 BSD-3-Clause 153 295 15 Updated Feb 24, 2025
  • homebrew-k Public

    K Homebrew tap

    Ruby 0 1 0 0 Updated Feb 24, 2025