Turn your complexity into confidence
Achieve compliance and save development time with mathematical rigor

What we do

Runtime Verification provides cutting-edge technology to design safe and secure systems and languages based on mathematically-grounded principles. Runtime Verification technology automatically and accurately detects the rarest, trickiest and most costly bugs lurking in your existing codebase or specifications.

Products & Services

K is a formal semantics framework for defining and designing programming languages and program analysis and verification tools for them.

RV-Match is a semantics-based dynamic analysis tool and debugger for C errors, and an automatic checker for all C undefinedness.

RV-Predict is an automatic predictive runtime analysis tool that detects a variety of Java and C concurrency errors without any false alarms.

RV-Monitor is a runtime monitoring tool that checks your Java code against formal specifications, with over 200 Java API properties built in.

Supporters & Contributors


K framework

Runtime Verification

Latest News and Events

Sep 21 2018 ERC777-K: Formal Executable Specification of ERC777 by Daejun Park
Aug 15 2018 Formal verification of ERC-20 contracts by Brian Marick
Jul 20 2018 How Formal Verification of Smart Contracts Works by Brian Marick
May 25 2018 K Framework – An Overview by Grigore Rosu
Mar 29 2018 Runtime Verification seeking experienced C and C++ engineers by David Young