Explore @runtimeverification Open Source projects

Runtime Verification Inc. (@runtimeverification)

runtimeverification

Stars
2,482
Global Org. Rank 7,959 (Top 3 %)
Registered over 11 years ago
Most used languages

Python
20.6 %

Java
17.5 %

C++
11.1 %

Solidity
9.5 %

Haskell
6.3 %

Makefile 6.3 %

TeX
6.3 %

Coq 4.8 %

HTML
4.8 %

WebAssembly 3.2 %

OCaml
1.6 %

C
1.6 %

Starlark 1.6 %

Shell
1.6 %

Standard ML 1.6 %

Rust
1.6 %
Location 🇺🇸 United States
Country Total Rank 4,084
Country Ranking

Solidity
9

WebAssembly 9

Coq 30

Haskell
114

Standard ML 151

Makefile 180

Starlark 189

TeX
307

OCaml
358

Java
769

HTML
996

C++
3,530

Python
8,215

Rust
8,883

verified-smart-contracts

Smart contracts which are formally verified

evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)

k

K Framework Tools 6.0

haskell-backend

The symbolic execution engine powering the K Framework

iele-semantics

Semantics of Virtual Machine for IELE prototype blockchain

publications

Publications of Runtime Verification, Inc.

wasm-semantics

A Prototype Formal Semantics of WebAssembly in K

erc20-semantics

javamop

Runtime verification system for Java, using AspectJ for instrumentation.

llvm-backend

KORE to llvm translation

plutus-core-semantics

algorand-verification

Formal verification of the Algorand consensus protocol

kontrol

deposit-contract-verification

beacon-chain-spec

Formalization of the Beacon Chain Phase 0 Specification in K

beacon-chain-verification

python-semantics

The semantics of Python in K

michelson-semantics

A K semantics of Tezos' Michelson language.

casper-proofs

Coq definitions and lemmas for verification of Casper

solidity

Fork of the Solidity Compiler for compiling Solidity to IELE

avm-semantics

rv-monitor

RV-Monitor core system code

foundry-upgradeable-contracts-examples

Example tests for exploring upgradeable contracts with Foundry

k-editor-support

Plugin files for editing K files

erc777-semantics

mpfr-java

GNU MPFR Java Bindings

zero-to-k-tutorial

pyk

Python tools for the K Framework

polkadot-verification

Verification of Polkadot WASM code

secureum-kontrol

blockchain-k-plugin

K plugin for IELE and KEVM

knock

Nock semantics in K

rdao-smc

A probabilistic rewriting model of Randao-based RNG schemes

bn128-ml

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

kavm-demo

elrond-semantics

foundry-demo

Foundry blog posts' executable demos

proof-generation

hs-backend-booster

Accelerates K Framework's Haskell backend

rv-android

Android runtime library for the RV-Monitor environment.

match

RV-Match issue tracker and releases

imp-semantics

The K semantics of IMP and associated tools

kup

K and Semantics Distribution Tool

predict

vlsm

property-db

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

k-vs-coq-language-frameworks

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

llvmmop

MOP framework for LLVM

khoon

gitbook-kontrol

CANtools

RV tools for reverse engineering the automotive CAN bus.

racy-c-programs

Benchmark of C/C++ programs exhibiting races.

rv-toolkit-docs

test-maven-deployment

Test - Delete me

rv-match_testing

z3k

C++ type inferencer for K using libz3

k-pldi-tutorial

Code supporting K tutorial session at PLDI 2023.

elrond-multisig

gitbook-kevm

rv-install

Unified installer for all Runtime Verification Inc. products

proof-checker-public

mir-semantics

kore-prof

Profiling utilities extracted from haskell-backend

RV-Log

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

mir-semantics-compiletest

Test suite for MIR semantics

gitbook-home

pl-tutorial

The K Programming Language Tutorial