Skip to content

@runtimeverification Runtime Verification Inc.

All

    Repositories list

    237 repositories

    • komet-node

      Public
      Local development testnet for Stellar based on K semantics
      Python
      •0•1•0•2•Updated Nov 1, 2026Nov 1, 2026

    • stellar-debugger

      Public
      Interactive breakpoint-style debugger for Stellar/Soroban
      TypeScript
      •
      BSD 3-Clause "New" or "Revised" License
      •1•3•0•12•Updated Oct 30, 2026Oct 30, 2026

    • haskell-backend

      Public
      The symbolic execution engine powering the K Framework
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •46•229•139•20•Updated Oct 29, 2026Oct 29, 2026

    • evm-semantics

      Public
      K Semantics of the Ethereum Virtual Machine (EVM)
      KCL
      •
      BSD 3-Clause "New" or "Revised" License
      •160•595•77•9•Updated Oct 28, 2026Oct 28, 2026

    • k

      Public
      K Framework Tools 7.0
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •164•600•310•16•Updated Oct 28, 2026Oct 28, 2026

    • rs-lending-xlm

      Public
      Soroban lending protocol on Stellar.
      Rust
      •
      Other
      •9•0•0•1•Updated Oct 27, 2026Oct 27, 2026

    • kontrol-node

      Public
      Kontrol node for testnet
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •0•0•18•12•Updated Oct 26, 2026Oct 26, 2026

    • rs-soroban-env

      Public
      Rust environment for Soroban contracts.
      Rust
      •
      Apache License 2.0
      •70•0•0•3•Updated Oct 22, 2026Oct 22, 2026

    • linux-ebpf-spike

      Public
      Lean
      •
      Other
      •0•0•0•0•Updated Oct 19, 2026Oct 19, 2026

    • kontrol

      Public
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •18•127•166•24•Updated Oct 15, 2026Oct 15, 2026

    • linux-cbpf-spike

      Public
      C
      •0•0•0•0•Updated Oct 15, 2026Oct 15, 2026

    • mir-semantics

      Public
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •5•55•73•18•Updated Oct 14, 2026Oct 14, 2026

    • simbolik-vscode

      Public
      VSCode extension for debugging Solidity using Simbolik API server
      TypeScript
      •
      BSD 3-Clause "New" or "Revised" License
      •4•48•16•7•Updated Oct 13, 2026Oct 13, 2026

    • kup

      Public
      K and Semantics Distribution Tool
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •2•10•18•8•Updated Oct 12, 2026Oct 12, 2026

    • skribe

      Public
      Property testing for Stylus smart contracts
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •0•31•1•6•Updated Oct 9, 2026Oct 9, 2026

    • komet-demo

      Public
      An example project for testing a simple contract using Komet
      Rust
      •0•1•0•3•Updated Oct 6, 2026Oct 6, 2026

    • komet

      Public
      WebAssembly
      •
      BSD 3-Clause "New" or "Revised" License
      •7•43•7•7•Updated Sep 16, 2026Sep 16, 2026

    • llvm-backend

      Public
      KORE to llvm translation
      C++
      •
      BSD 3-Clause "New" or "Revised" License
      •22•43•41•1•Updated Sep 14, 2026Sep 14, 2026

    • wasm-micro-runtime

      Public
      WebAssembly Micro Runtime (WAMR)
      C
      •
      Apache License 2.0
      •880•0•0•0•Updated Sep 10, 2026Sep 10, 2026

    • linux-isolation-spike

      Public
      Formal verification spike on Linux kernel isolation primitives for AI-agent sandboxing
      Lean
      •0•1•0•0•Updated Sep 9, 2026Sep 9, 2026

    • soroban-examples

      Public
      Example Soroban Contracts
      Circom
      •
      Apache License 2.0
      •171•0•0•4•Updated Aug 31, 2026Aug 31, 2026

    • verify-rust-std

      Public
      Verifying the Rust standard library: Runtime Verifiction introduces KMIR!
      Rust
      •
      Other
      •17k•0•0•2•Updated Aug 20, 2026Aug 20, 2026

    • publications

      Public
      Publications of Runtime Verification, Inc.
      HTML
      •20•97•0•0•Updated Aug 18, 2026Aug 18, 2026

    • stellar-facilitator-bazaar

      Public
      0•0•0•0•Updated Aug 17, 2026Aug 17, 2026

    • stable-mir-json

      Public
      KMIR Rust Library
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •6•11•29•16•Updated Aug 15, 2026Aug 15, 2026

    • uvc-frame-size-overflow

      Public
      Reproducer: 32-bit signed wraparound in dwMaxVideoFrameBufferSize in the Linux UVC descriptor parser
      linux-kerneluvcreproducer
      linux-kerneluvcreproducerinteger-overflow
      C
      •
      BSD 3-Clause "New" or "Revised" License
      •0•1•0•0•Updated Aug 14, 2026Aug 14, 2026

    • kernel-rust-verification-spike

      Public
      Feasibility spike: extracting Linux kernel Rust parsers (Binder) into LLBC via Charon, toward Lean 4 verification
      Lean
      •
      GNU General Public License v2.0
      •1•3•1•0•Updated Aug 12, 2026Aug 12, 2026

    • wasm-semantics

      Public
      A Formal Semantics of WebAssembly in K
      WebAssembly
      •
      Other
      •26•107•26•1•Updated Aug 12, 2026Aug 12, 2026

    • imp-semantics

      Public
      The K semantics of IMP and associated tools
      Python
      •1•7•0•3•Updated Aug 10, 2026Aug 10, 2026

    • riscv-semantics

      Public
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •0•7•21•3•Updated Aug 10, 2026Aug 10, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.