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.

If you ended up in this blog post, you are probably somehow familiar with K framework, wanting to learn more, or trying to address some doubts. Well, I’m glad to say that you came to the right place. …


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 framework. The CamlCase team is taking security seriously, as evidenced by the myriad of verification efforts and audits they have performed, including:

  • Trail of Bits conducted an audit for the Dexter v1 smart contract, the Dexter frontend v0.8.2, and the Morley Framework implementation of the contract.
  • CamlCase team conducted extensive…


By Silvia Barredo and Musab Alturki

Runtime Verification is thrilled to announce XET token audit completion. XET token is the utility and governance token of the Xfinite ecosystem, a blockchain platform redefining the future of digital on-demand entertainment.

XET Token’s Audit Scope

XET token is the native currency of the Xfinite ecosystem. The token functions as a unique value of exchange and governance mechanism for all stakeholders including users, brands, influencers, and content producers. XET is implemented as an Algorand Standard Asset (ASA), a Layer-1 mechanism to represent any type of asset on the Algorand blockchain.

The audit focused on checking the consistency of the specification of the XET token…


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 threats affecting staking providers and other DeFi projects.

DeFi, a paradise for hackers

Over the past year and a half, DeFi has experienced exponential growth with more than 2.9 million users at the time of writing this blog post, and it doesn’t show any signs of slowing down.

Many DeFi projects have been born in…


Runtime Verification, a startup that uses runtime verification-based techniques to conduct security audits on virtual machines and smart contracts, has raised $5.3 million in a funding round led by IOSG Ventures.

Investment came from a range of notable VC firms including Fenbushi Capital, Maven 11, Borderless Capital (Algorand), cFund (Cardano) managed by Wave Financial, Hypersphere (Polkadot), Elrond Research, and Tezos Foundation.

With involvement from the accelerator programs of five major blockchains, the fundraiser validated Runtime Verification’s dynamic software analysis approach to securing systems in the cryptocurrency industry.

The funds raised will be used to accelerate the development of tooling intended…


by Rikard Hjort

Elrond and Runtime Verification started as friends, professional admirers of each other’s organizations. The picture attached to this post shows members of both companies together at DevCon IV in Prague, October 2018. Quickly thereafter, Grigore Rosu, Runtime Verification’s founder and CEO, agreed to become an advisor to Elrond.


by Stephen Skeirik

The Power of Reachability Logic

In a previous blog post, we introduced the K-Michelson project, a project developed by Runtime Verification and funded by a generous grant from the Tezos Foundation. So what is K-Michelson? Simply put, it is a formal verification framework for Michelson smart contracts; see our previous post for details. 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 the first part of the series, we considered point how the K Framework is an example of point (1) using our K-Michelson tool as a concrete example. …


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, we limit our focus to question (1). So, what should an ideal programming language specification look like? Several properties come to mind:

  • Clarity: it should be unambiguous and straightforward.
  • Completeness: It should be self-contained and describe how all possible programs execute.
  • Testability: arbitrary programs should be executable against the specification…


by Musab A. Alturki

We are pleased to announce that Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts. The grant is part of its recently launched 250 Million ALGO Ecosystem Grants Program, a multi-year program that aims to support research and development of the Algorand ecosystem. We are very excited to have the opportunity to collaborate with Algorand in forming the future of Algorand’s smart contract architecture and supporting its growing community of developers. …


by Stephen Skeirik

Runtime Verification Inc. (RV) is pleased to announce that we are partnering with the Tezos Foundation via the Tezos Ecosystem Grants program to develop a formal verification framework for the Michelson smart contract language! From its inception, the Tezos blockchain was designed with convenience, security, and extensibility in mind. However, unlike the status quo of predecessor technologies like Bitcoin, the true vision of a thriving Tezos ecosystem is more than just a secure digital currency exchange―it is a platform for developing and publishing distributed applications via smart contracts using its smart contract language Michelson. …

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