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

Security Audits icon

Security Audits

A comprehensive code and/or design review to check for bugs, vulnerabilities, attack vectors, common anti-patterns, code smells.

Formal Verification icon

Formal Verification

The highest level of guarantee that can be achieved for a codebase. We prove that the code will always behave as expected.

ERCx icon

ERCx

Check your ERC functional compliance and test your desirable properties before and after deploying it on Mainnet.

Design Review icon

Design Review

Errors in design are the most critical and the most costly to fix, so it’s best to catch and correct them early.

Code Review icon

Code Review

We review your codebase, ensuring that it conforms to the specifications produced in the Design Review.

Protocol Verification icon

Protocol Verification

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

Featured Reports

Synonym Finance
Synonym Finance
Security Audit
Ethereum Foundation
Ethereum Foundation
Formal Verification
Morpho
Morpho
Security Audit
Hydra CX
Hydra CX
Security Audit
Gnosis Safe
Gnosis Safe
Formal Verification
Band Protocol
Band Protocol
Security Audit

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