At Runtime Verification, K framework is the backbone of the company. Since the CEO of Runtime Verification, Grigore Rosu, started the K project back in 2003 for teaching purposes, the K framework has evolved, its user base has grown, and there are more use cases than ever in the ecosystem.

By Sylvia Barredo

Runtime Verification is thrilled to announce Dexter 2’s formal verification completion. Dexter 2 is an open-source, decentralized, non-custodial exchange for XTZ and FA1.2/FA2 tokens on the Tezos blockchain developed by the CamlCase team.

Dexter’s Security Efforts

Dexter’s engagement focused on formally verifying the bytecode using K-Michelson, an implementation of Michelson in the K…

By Silvia Barredo and Daejun Park

Over the past eight months, a series of companies have undergone smart contract security audits with Runtime Verification. These companies have something in common: they are staking providers operating in the DeFi ecosystem.

This blog post aims to explain some common mistakes, patterns and aims to create awareness about security…

by Stephen Skeirik

In a previous post, we introduced the K-Michelson project, a formal verification framework for Michelson smart contracts, and described our overall project goals. In this two-part series, we will investigate:

  1. What an ideal programming language specification looks like.
  2. How this ideal framework powers nextgen program testing.

In this first part…

Runtime Verification

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store