Runtime Verification website heroRuntime Verification website hero

We love formal methods

We specify, model and verify code and designs using formal logic.
Properties can be anything you can specify in logic. It can range over a function, or an entire program.
We check those properties against concrete inputs (runtime verification) and symbolic inputs (formal verification), and explore all possible behaviors of the code, to give you the highest possible assurance.

Our approach is based on the  K Semantic Framework.

What We Offer

Smart contract verification icon

Smart contract verification

Prove the correctness of smart contracts compiled for the Ethereum and Cardano virtual machines.

NFT Checker icon

NFT Checker

Mints can be gamed, tokens can be stolen, gas can be wasted, and bad code makes people wary of rug pulls.

Protocol verification icon

Protocol verification

Increase confidence in the correctness and security of the decentralized system powered by your protocol.

Blockchain advisory services icon

Blockchain advisory services

Receive targeted advice from an RV senior engineer on the verification topic of your choice: smart contracts, tokens, protocols, or virtual machines.

Firefly icon

Firefly

Firefly is a set of quality assurance tools for Ethereum smart contracts aimed to help developers before the audit and formal verification stages.

ERCx icon

ERCx

Check your token’s full functional compliance with the ERC20 standard and desirable properties before and after deploying it on MainNet.

Partners & Customers

Alchemix
Algodex
Algofi
Algorand
AshSwap
Atlendis
Bihu
Blockswap
Casper protocol
Cosmos
Cryptape blockchain
Dapper Labs
DENSO
Dexter
Element Finance
Emurgo
Ethereum
Ethereum Community Fund
Ethereum Enterprise Alliance
Ethereum Trust Alliance
EXA Finance
Folks Finance
Galactic
GigaStar
Gnosis
Gyroscope
Hatom
Hone
HydraDX
IOHK
Maker
Membrane Finance
Morpho
MultiversX
NASA
NSF
Ojo
Olympus DAO
Pact
Panvala
Parity
PlatON
Polkadot
PON Network
QuipuSwap
Stakefish
StakerDAO
StakeWise
SundaeSwap
Swaap
Swell Network
Tempus blockchain
Term Labs
Tezos
Tinyman
Toyota ITC
Tracer
Umee
Uniswap
Web3 Foundation
Whiteblock
World Mobile
xBacked
Xfinite
Yieldly
Zivoe
Zorp

Testimonials

Investors

Borderless Capital
Fenbushi Capital
Hypersphere
IOSG
Maven 11
MultiversX
Tezos Foundation (Investor)
Wave Financial