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.

Protocol verification icon

Protocol verification

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

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
Band Protocol
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
Synonym Finance
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