Discover runtimeverification/knock Open Source project

K Semantics of the Ethereum Virtual Machine (EVM)

717

evm-semantics

507

K Framework Tools 7.0

The symbolic execution engine powering the K Framework

447

haskell-backend

Semantics of Virtual Machine for IELE prototype blockchain

210

iele-semantics

HTML

130

publications

Publications of Runtime Verification, Inc.

HTML

wasm-semantics

A Prototype Formal Semantics of WebAssembly in K

WebAssembly

kontrol

Runtime verification system for Java, using AspectJ for instrumentation.

erc20-semantics

ERC20 in K

javamop

llvm-backend

KORE to llvm translation

deposit-contract-verification

plutus-core-semantics

Formal verification of the Algorand consensus protocol

algorand-verification

Coq

beacon-chain-spec

Formalization of the Beacon Chain Phase 0 Specification in K

The semantics of Python in K

python-semantics

beacon-chain-verification

A K semantics of Tezos' Michelson language.

michelson-semantics

Coq definitions and lemmas for verification of Casper

casper-proofs

Fork of the Solidity Compiler for compiling Solidity to IELE

solidity

RV-Monitor core system code

rv-monitor

avm-semantics

Python tools for the K Framework

pyk

Example tests for exploring upgradeable contracts with Foundry

foundry-upgradeable-contracts-examples

Foundry blog posts' executable demos

kontrol-demo

zero-to-k-tutorial

Plugin files for editing K files

simbolik-vscode

TypeScript

k-editor-support

erc777-semantics

mpfr-java

GNU MPFR Java Bindings

Solady formal verification with Kontrol

kontrol-solady

Verification of Polkadot WASM code

polkadot-verification

WebAssembly

secureum-kontrol

Cheatcodes library for your symbolic Kontrol tests

kontrol-cheatcodes

K plugin for IELE and KEVM

blockchain-k-plugin

BN 128 elliptic curve implementation in OCAML (for Ethereum zero-knowledge proofs)

bn128-ml

OCaml

mx-semantics

A probabilistic rewriting model of Randao-based RNG schemes

rdao-smc

Accelerates K Framework's Haskell backend

hs-backend-booster

proof-generation

K and Semantics Distribution Tool

kup

kavm-demo

Android runtime library for the RV-Monitor environment.

rv-android

RV-Match issue tracker and releases

match

gitbook-kontrol

imp-semantics

The K semantics of IMP and associated tools

An annotated Java API and a tool for generated documentation augmented with properties.

predict

vlsm

Coq

property-db

The K Programming Language Tutorial

k-vs-coq-language-frameworks

Coq

pl-tutorial

Standard ML

rv-predict

Code for improved rv-predict and installer

evaluation

Evaluation results of RV tools and comparisons with other tools

rvmatch-eclipse-plugin

kontrol-tutorial

khoon

CI Hosting Symbolic Execution for Ethereum-Optimism

optimism-ci

llvmmop

MOP framework for LLVM

RV tools for reverse engineering the automotive CAN bus.

CANtools

rv-toolkit-docs

HTML

racy-c-programs

Benchmark of C/C++ programs exhibiting races.

C++ type inferencer for K using libz3

test-maven-deployment

Test - Delete me

rv-match_testing

Shell

z3k

Code supporting K tutorial session at PLDI 2023.

k-pldi-tutorial

Shell

elrond-multisig

Starlark

gitbook-kevm

proof-checker-public

mir-semantics

Profiling utilities extracted from haskell-backend

kore-prof

Frontend for feeding log files and other precomputed event traces to RV-Monitor.

RV-Log

Test suite for MIR semantics

mir-semantics-compiletest

Rust

gitbook-home

riscv-gnu-toolchain-images

Docker image builds for the RISC-V GNU toolchain

Dockerfile

nailgun

Nailgun is a client, protocol, and server for running Java programs from the command line without incurring the JVM startup overhead.

ercx-vscode

VSCode support for ERCx

TypeScript

simbolik-examples

Unified installer for all Runtime Verification Inc. products

rv-install