pr-502.sandbox.runtimeverification.com Open in urlscan Pro
3.13.106.47  Public Scan

Form analysis
0 forms found in the DOM

Text Content

Open main menu
about
 * Company
 * Team
 * Videos
 * FAQ

services
 * Formal Verification
 * Smart Contract Auditing
 * Security Consulting

products
 * ERCx
 * K
 * KaaS
 * Kasmer
 * Kontrol
 * Simbolik

research
blog
CONTACT US



TAKE YOUR SECURITY TO THE NEXT LEVEL

Instead of paying researchers to look for bugs, verify your smart contracts are
bug-free with formal verification.
We explore all possible behaviors of the code, to give you the highest possible
assurance.
Ship FAST with continous integration of proofs,
and outsource the compute to us using K as a Service (Kaas).
Our approach is based on theK Semantic Framework


START VERIFYING FOR FREE

Formal Verification can cost less than a traditional audit. You can write proofs
in Solidity or Rust, or use your existing Foundry tests.

GET STARTED



FORMAL VERIFICATION

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

Formal Verification


K AS A SERVICE

Cloud Based and CI Integrated simbolic execution delivery platform, optimized
for smart contract formal verification.

Buy Compute Power


SECURITY AUDITS

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

Security Audits


LEARN ABOUT OUR IMPACT ON WEB3 SECURITY

We have been auditing smart contracts since 2018 and love sharing what we learn.
Browse our articles and learn about web3 security from one of the most
experienced teams in crypto.

VIEW ALL ARTICLES


CATEGORIES

All ArticlesAuditsKERCxNewsSmart ContractsVerification
Kontrol Integrated Verification of the Optimism Pausability Mechanism
by Runtime Verification
May 16th, 2024
Read More
K 7.0: Improving K for Ecosystem Tool Developers
by Bruce Collie
May 8th, 2024
Read More
Runtime Verification Hosts EthCluj Workshop on Formal Methods
by Raoul Schaffranek
May 6th, 2024
Read More
Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct
by Juan Conejero
April 2nd, 2024
Read More

VIEW ALL ARTICLES


PARTNERS & CUSTOMERS

Featured reports
Ethereum Foundation

Formal Verification

Optimism

Formal Verification

Gnosis Safe

Formal Verification

Uniswap

Formal Verification

Morpho

Security Audit

Synonym Finance

Security Audit


BROWSE OUR WORK


INVESTORS




TESTIMONIALS

Now we are happy to announce the completion of an extra layer of security:
"formal verification". It was a huge effort by @rv_inc and done with support
from @ethereumecf. Gnosis will soon start moving funds to this verified version
of the contract.



Martin Köppelmann@koeppelmann

I'm excited to be working with Runtime Verification @rv_inc again. We just
signed a seven figure deal to restart work on IELE. Welcome back K, we missed
you.



Charles Hoskinson@IOHK_Charles

$EGLD gets formal verification tools from @rv_inc With otherwise expensive &
complex testing tools available in the MultiversX devkit the overall security of
our DeFi ecosystem raises to meet institutional-grade requirements.



MultiversX eGold@MultiversX

The work been done by @rv_inc, it’s incredible. I only have good things to say
and the more I learn about K-Framework, the more ideas I get to bring even more
innovation to @Cardano 💪 #cardano



Nico Arqueros@NicoArqueros

The first ever ERC20 formal verification spec was done by @rv_inc they now made
one for ERC777 as well! The next token standard. Now we need automated gen.
proofs and checkers to run those!



Fabian Vogelsteller@feindura

@ercwl @rv_inc Yeah, the KEVM is amazing. We also built
https://github.com/dapphub/klab to be able to explore the complete space of
execution paths for an ethereum contract. Browser version in the pipeline!



Martin Lundfall@MartinLundfall

This report on @rv_inc's verification of RANDAO's possible randomness bias under
worst-case adversarial conditions using statistical model checking is one of the
most underrated new papers in cryptocurrency security/modeling, IMO.
rdao-analysis.pdf



Philip Daian@phildaian

To make the Gnosis Safe one of the most secure multisigs on the market, we
worked with formal verification pros @rv_inc and updated our smart contracts.
Check out the full report here 👉
GnosisSafe_RuntimeVerification.pdf



Gnosis Safe@gnosisSafe

Another major achievement is the Meta VM MultiversX brings by building a GO
backend to K framework. Through this we will support 3 VMs at the same time for
max flexibility: EVM, WASM, IELE + formal verification



Beniamin Mincu ⚡@beniaminmincu

Warming up to proposing the Jello Paper as the canonical EVM spec, and would
love everyone's thoughts. IMO the Jello Paper way clearer and complete versus
the current Yellow Paper. Kudos to the KEVM folks 🎉
https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389



Brooklyn Zelenka 🏳️‍🌈@expede

Just released v0.11.3 with critical bug fix to the eth2 state transition spec.
Special thanks to @daejunpark for finding the bug while doing formal
verification on the eth2 spec for @rv_inc!
https://github.com/ethereum/eth2.0-specs/releases/tag/v0.11.3



Danny Ryan@dannyryan

@rv_inc! completes the formal verification of the eth2 deposit contract
bytecode!
https://github.com/runtimeverification/verified-smart-contracts/blob/master/deposit/bytecode-verification/deposit-spec.ini



Danny Ryan@dannyryan

Honestly, @rv_inc was incredible to work with. They were incredibly thorough,
thoughtful and dilligent in the entire process. We're looking forward to
continuing work with them and a special callout to @daejunpark.



Will Villanueva@wjvill

Giskard Protocol (CBFT) was formally verified by @rv_inc. It should be a
technical requirement for the industrial adoption of any innovative public
ledger.



Chen Li@ChenLLII




CONTACT US

Your Information *



What kind of a request do you have? *

AUDIT REQUESTGENERAL INQUIRY

What services are you interested in? *

 * Formal Verification

 * Security Audit Report

 * Design Review

 * Code Review

 * Dev Ops

 * Other

Project description *

What is your ecosystem? *

AlgorandCardanoCosmosEthereumMultiversXPolkadotSolanaTezosOther

What is your approximate deadline for completing this work? *

How many lines of code do you need audited? *

What is your approximate budget in USD?

Have you used any tools for testing?

Yes
No

Has this code been audited before?

Yes
No

Are you able to share a link to your repository?


WORK WITH US

Company

Resources

Connect

Mission and Vision|Presentations|Careers|News|Publications|Partnerships|Media
Kit|



Events

333 North Green Street, Chicago, IL

2024 © all rights reserved | privacy policy | terms of use