We don't like to brag, but we are collecting what other folks write about our work (reverse chronologically). If you would like to receive all the RV News on regular basis, please subscribe here.
“I am very pleased that our investors have embraced our unique
language-parametric approach, built over more than 20 years within
the K Framework. The generality of our approach allows our tools
to be easily configured to work with different programming
languages and different blockchains. The fact that five
blockchains joined our investment round through their funds, based
on research from their development teams who witnessed our
technology, is a testament to the universality and strength of our
K-powered technology.” -
Grigore Rosu, Founder and CEO Runtime Verification
Full post
“As someone who was fighting cybersecurity risks on a daily basis,
I’d always been looking for the “ultimate” solution to the arms
race between the adversaries and the defenders, until I met with
formal verification. It completely shifts the paradigm from
looking for potential loopholes to certifying a software program
is correct and thus “bug-free”. It is the “holy grail” of software
security. Runtime Verification is a cross-industry leader in the
quest to such “holy grail”. By carefully designing technology,
framework, and tools to apply the mathematical rigor to software
programs, it has made formal verification ever more practical.
Critical software and infrastructure in the aerospace and
automobile industries has been benefiting from it in the past
decade. Now with the thriving decentralized economy, Runtime
Verification has applied their technology to safeguarding some of
our most frequently used blockchain infrastructures and
applications as well. We are truly excited to work closely with
Runtime Verification and embark on the next journey to take formal
verification to our everyday software systems.” -
Xinshu Dong, Partner IOSG Ventures
Full post
“Security is key for DeFi to mature even further. We cannot expect
this to grow to a trillion dollar industry without institutional
grade security. Runtime Verification provides exactly that. By
using formal verification they go a step further than other audits
and provide security while working alongside teams. We are excited
to kick off the next growth phase for the company.” -
Balder Bomans, Managing Partner Maven 11 Capital
Full post
“We are excited about being able to secure a voice for the Elrond
Network at the heart of developing what we believe to be essential
tools for the advancement of the general blockchain space. Our
strategic investment in Runtime Verification aims for the
sustainable growth of methodologies and devkits that already are
embedded into the core practices involved in building the Elrond
protocol and connected tools.” -
Beniamin Mincu, CEO Elrond Network
Full post
“After several months of working together, we already were able to
create a K-Framework replica of our Arwen VM dubbed KArwen. Arwen
is a WASM VM so Runtime Verification was able to expand their
KWasm semantics for WASM to accommodate our virtual machine. The
resulting KArwen is a fully formalized auto-generated virtual
machine that can execute Elrond Smart contracts. This lays the
groundwork for advanced formal tooling to be used for the Elrond
smart contracts. An important outcome is also that Mandos testing
using the K Framework already allows developers to perform code
coverage testing at a lower level than previously possible.” -
Elrond
Full post
“Mantis will also use Runtime Verification’s ‘K’ framework to give
more sophisticated techniques for smart contracts verification and
more predictable gas costs, making the platform more appealing,
both to developers building smart contracts and end users looking
for a cost-effective secure blockchain platform.”
Full post
“We are happy to announce that the Batch Deposit Contract has
officially been audited by Runtime Verification. Specifically, we
have worked closely with Daejun Park of Runtime Verification, who
has previously conducted an
end-to-end formal verification
of the Ethereum 2.0 deposit smart contract, to conduct this audit.
We want to thank the Runtime Verification team for being diligent,
helpful, and extremely responsive throughout the engagement.”
Full post
“Quantstamp’s experience includes securing over 5 billion USD
worth of digital assets and working with over 140 startups,
foundations, and enterprises. Quantstamp chose to develop the
Hedera Hashgraph stablecoin standard in the
K framework because
it is robust, extensible, and widely adopted amongst developers.
The framework shortens development time, provides formal
guarantees about the correctness of functions, removes the need to
develop new tests, and creates a shared understanding amongst
developers concerning the architecture and functionality of
implemented stablecoins. When stablecoins follow a secure
framework, the framework facilitates the integration of
implemented stablecoins into other financial applications. This
type of modularity is the ideal environment to encourage the
development of a healthy stablecoin ecosystem for enterprises.”
Full post
“It was a great experience to work with RV engineers and
scientists on the Griskard proof. I was very impressed by the
team's ability to tackle complicated concurrent scenarios and edge
cases. I am happy to have RV as part of PlatON's grand plan.
Moving forward, there are plenty of opportunities to engage again,
namely around protocol modeling and formal verification of smart
contracts.” - James Qu, CTO PlatON
Full post
“IELE is one in every of my favorite initiatives. It’s
unbelievable stuff, it’s actually thrilling and I feel it gonna
open up an entire new dimension of the product and I all the time
believed that. After the nice collapse of 2017 we had nice-to-have
vs. must-have and that was within the nice-to-have column. Plutus,
Marlowe and this stuff are within the must-have column.” -
Charles Hoskinson, CEO IOHK
Full article
“Runtime Verification’s solution is to apply its K Framework,
which is a mathematically rigorous toolset that gives users the
ability to design and implement programming languages from basic
principles, and derive software analysis tools for them following
a correct-by-construction methodology. These factors allow users
of the K framework to ultimately verify their programs and systems
for maximum assurance.” - Illinois CS
Full post
“We are delighted to support Runtime Verification’s grant
application,” said Sean Lee, CEO of the Algorand Foundation. “We
believe that creating a
formal framework for Algorand Smart Contracts (ASC1s) will
enable the creation of innovative, secure, and reliable DAPPs and
DeFi solutions on the Algorand blockchain.” -
Algorand Foundation
Full post
“Runtime Verification designs formal models for high-value
application domains, then uses the models to develop
domain-specific products and services focused on correctness and
security. Building off of its
previous Tezos work, Runtime Verification will create a
formal verification framework for Michelson by extending
its existing unit testing framework to handle the case of symbolic
unit tests. This project will help make it easier for developers
of all backgrounds to deploy secure Tezos smart contracts.” -
Tezos Foundation
Full post
“We propose a new verification method for software intended to be
flown on unmanned aircraft systems that is both automatic and
inexpensive. In Phase 1 we will focus on a class of errors in C
programs called “undefined behavior” (UB) because this makes the
method both easy to use and easy to compare with existing static
analysis tools.” - NASA SBIR
Grant description
“Formal specifications and proofs of method-level correctness for
the smart contracts in the uniswap-v2-core repository (namely
UniswapV2Pair and UniswapV2Factory) were produced using the act
specification language and K framework. [...] Formal
specifications for the contracts in uniswap-v2-core were written
in the act specification language. These specifications are then
compiled into reachability claims in the K language, and
proved using the K framework prover against the bytecode produced
by the build system in the uniswap-v2-core repository.” -
Dapp Labs
Full report
“To say we are excited to engage with PlatON Networks is an
understatement. We began conversations with their team in late
2019 about how and where our two companies could engage. Although
we discussed various opportunities, including those related to
writing and verifying programs written in web assembly (WASM), we
eventually settled on protocol verification as a good place to
start what will hopefully become a long-term collaboration and
partnership.” - Patrick MacKay, COO
Full post
“Today we are very pleased to announce the formation of the
Ethereum Trust Alliance (ETA). The ETA is a group of global
blockchain security companies that are creating a security rating
system for smart contracts to help users gain greater awareness of
smart contract security and differentiate contracts which have
gone through rigorous security checks. The founding members are
MythX, Quantstamp, Runtime Verification, Sooho, SmartDec
and ConsenSys Diligence.” - Ethereum Trust Alliance
Full post
“Runtime Verification is a company aimed at using runtime
verification-based techniques to improve the safety, reliability,
and correctness of software systems. The purpose of this grant is
to develop a formal semantics and reference implementation of
Michelson, a domain-specific language for Tezos smart
contracts, in the K Framework. The K language is designed
to make language definitions as readable as possible while still
ensuring a K semantics has a precise mathematical meaning, and is
supported by the tools of the K Framework. The Runtime
Verification team will also publish documentation and interact
with the wider Tezos developer community as part of this project.”
- Tezos Foundation
Full post
“The design and implementation of bridges to all major blockchains
is one of our highest priorities. [...] Currently, the only way to
generate a Polkadot Runtime is by using Rust along with
Parity-built tools. We would like to increase the language options
for developers to write these Runtimes and recently released an
RFP for the development of a tool to generate WebAssembly Runtimes
from AssemblyScript.” - Web3 Foundation
Full post
“The Elrond research and development team will work closely with
Runtime Verification to further develop the
K framework and its capability to generate
correct-by-construction Virtual Machines for the blockchain.
Through the research and development initiative between Elrond and
Runtime Verification we aim to take smart contracts to the next
level, and to make the GO backend developed by Elrond for the K
framework, open source and available to the wide public.” -
Elrond Network
Full post
“To achieve even greater assurance about the Algorand protocol,
and to make future design and validation of new protocols easier,
we have chosen to enhance our mathematical proofs on paper with
machine-checkable formal verification approaches. For this
purpose, we engaged Runtime Verification, a company with
deep verification expertise, to verify the correctness of the
Algorand consensus protocol.” - Algorand Foundation
Full post
“Many resources are shifting into testing, fuzzing, and audits
over the coming months. We engaged Runtime Verification to
formally verify the deposit contract and to formally
specify the Beacon Chain. This is in addition to
considerable effort by the research, development, and security
teams involved in ETH 2.0 toward reliability and security.” -
Ethereum Foundation
Full post
“Our team worked closely with Runtime Verification (RV) — a
company that specializes in using runtime verification techniques
to ensure that software systems are secure — to release a formal
verification report. While testing and auditing are essential
steps in the development process, formal verification is a
mathematical proof-based methodology used to significantly
decrease the likelihood that a smart contract is buggy.” -
Gnosis
Full post
“Runtime Verification has been working closely with Rikard
Hjort of Chalmers University on the KWasm semantics, which
will allow Web Assembly contracts to be formally verified
using the K framework. The core computational opcodes are
finished, what remains are memories, tables, and modules. Memories
are almost done, awaiting final review and approval, and tables
will follow shortly.” - Panvala
Full post
“Runtime Verification, based in Urbana, has developed tools
to improve the safety and reliability of software systems. Its
technology can automatically detect bugs that are lurking in a
company’s software, and identify problems before a program
crashes. Runtime’s customers include a handful of high-profile
clients—such as Boeing, NASA, Toyota and the
National Science Foundation—who use the startup to make
sure their code is error free. For these types of companies, if
their software fails, the stakes are higher than, say, a shopping
app or a dating website. Detecting problems as soon as possible
helps machines run better and keeps people inside those machines
safer.” - Chicago INNO
Full post
“Uniswap liquidity pools are autonomous and use the Constant
Product Market Maker (x*y=k). This model was formalized and the
smart contract implementation passed a lightweight formal
verification.” - Uniswap
Full post
“To provide the highest confidence that the contracts behave as
expected, we are working with Runtime Verification to
provide us with a formal and mathematically provable audit of the
Multi-Collateral smart contracts. We believe MakerDAO will
be the first production smart contract system that is formally
verified in this manner.” - Maker
Full post
“The K framework was used to formally model the semantics
of the Ethereum Virtual Machine, and the knowledge gained from
this process was employed to design IELE, the virtual
machine for Cardano that will be released in a test format in a
few weeks’ time. This is the first time this technology has been
deployed within the blockchain industry. Importantly, K is a means
to formally verify the code of smart contracts, so they can be
automatically checked for the types of flaws that have led to
catastrophic financial loss, and must be avoided at all costs.” -
Cardano Foundation
Full post
“The first Cardano smart contracts testnet launches today, the
KEVM testnet, a correct by construction version of the
Ethereum Virtual Machine (EVM) specified in the
K framework. This technology, produced by
Runtime Verification with the support of IOHK, is the first
time that a complete formal semantics of the EVM have been
produced. This is an important first in cryptocurrency that is a
necessary step towards the promise of third-generation
blockchains.” - IOHK
Full post
“These grants will fuel the
teams working hard at research & development to support the
entire ecosystem. Furthermore, we hope that these grants will
signal to the community what we think are the missing pieces in
the ecosystem that need more support. Said in another way, the
Foundation is here to serve teams and individuals that are working
to prevent a tragedy of the commons.” -
Ethereum Foundation
Full post
2021-06-22 | Elrond Network | Commitment Towards Institutional Grade Security: Elrond Joins Runtime Verification Series A Funding Round
2021-06-22 | 链闻 ChainNews | 三分钟读懂区块链安全审计机构 Runtime Verification 形式化验证方案
2021-06-21 | IOSG Ventures | 为什么我们领投 Runtime Verification
2021-06-20 | AlexaBlockchain | Security Audit Firm Runtime Verification Raises $5.3 Million
2021-06-19 | IOSG Ventures | Runtime Verification: The Game Changer for Securing Blockchain
2021-06-18 | Maven 11 Capital | Maven 11 Capital backs Runtime Verification
2021-06-18 | CoinDesk | Security Audit Firm Raises $5.3M From Funds Investing in Polkadot, Cardano Blockchains
2021-06-18 | Illinois CS | Runtime Verification Raises $5.3 Million To Advance Blockchain Security
2021-06-18 | CoinQuora | Runtime Verification Raises $5.3M for Better Blockchain Security
2021-06-18 | Investing.com | Runtime Verification Raises $5.3M for Better Blockchain Security
2021-06-18 | U.Today | Blockchain Security Auditor Runtime Verification Raises $5.3 Million
2021-06-18 | Yahoo News | Security Audit Firm Raises $5.3M From Funds Investing in Polkadot, Cardano Blockchains
2021-06-18 | 币世界 Bi Shi Jie | 安全审计机构 Runtime Verification 完成530万美元融资,由IOSG领投
2021-06-18 | 链闻 ChainNews | 安全審計機構 Runtime Verification 完成 530 萬美元融資,IOSG Ventures 領投
2021-06-18 | 律动 BlockBeats | Security system developer Runtime Verification closed a $5.3 million funding round, led by IOSG Ventures
2021-06-18 | THE BIT BUZZ | Runtime Verification Raises $ 5.3M to Improve Blockchain Safety | Pc science
2021-01-06 | Elrond Network | From Rockets To Blockchains: Formal Verification Pioneered At NASA Applied At Elrond Via Runtime Verification
2020-12-23 | Crypto Slate | IOHK’s new KEVM devnet opens up Cardano for Ethereum developers
2020-12-21 | Digital Coin Standard | K framework Ensures Compatibility Between Solidity And Cardano’s Blockchain For Interoperability
2020-12-18 | Fintech Zoom | Ethereum – Cardano to speak in confidence to Ethereum Solidity devs with new initiative
2020-12-18 | Blockchain Technology News | Cardano is building bridges to Ethereum with new KEVM testnet
2020-12-11 | Illinois CS | Abdelzaher, Lazebnik, and Rosu named 2021 IEEE Fellows
2020-12-11 | Bankless Times | IOHK Relaunches Mantis, Targets Ethereum Classic community
2020-12-11 | FinTech Zoom | IOHK relaunches Mantis to supply Ethereum Basic neighborhood a safer future
2020-12-08 | PlatON Network | The Safety and Stability of PlatON Consensus Protocol Passed Runtime Verification’s Academic-Level Scrutiny
2020-12-04 | Crypto Ninjas | IOHK plans to achieve future Cardano smart contract compatibility with all programming languages
2020-12-04 | INVEZZ | Cardano (ADA) smart contract now compatible with all programming languages
2020-12-04 | Business Blockchain HQ | Cardano Introduces Two Devnets to Enable Any Developer to Build Smart Contracts and Dappss
2020-11-22 | Crypto News Flash | Cardano: Update on financial contracts, Goguen, Marlowe and Plutus
2020-11-16 | Stake.Fish | Getting closer to launch: The stakefish Batch Deposit Contract audit is complete
2020-10-28 | Quantstamp Labs | Formally Verifying Hedera Hashgraph's Stablecoin Framework
2020-10-26 | PlatON Networks | Runtime Verification completes another successful engagement with PlatON Networks
2020-10-12 | New World Times | IOHK indicators contract with Runtime Verification
2020-10-11 | Crypto News Flash | Cardano: IOHK signs contract with Runtime Verification, roadmap for Goguen to be released end of October
2020-10-08 | Illinois CS | Rosu sharpens company vision with third NASA SBIR grant
2020-07-30 | Illinois CS | Sha models a more certain way forward for medical treatments during COVID-19 pandemic
2020-07-29 | Algorand Foundation | Runtime Verification Inc are the latest recipient of an Algorand Foundation Grant
2020-07-23 | Tezos Foundation | Announcing Fourth Cohort of Tezos Ecosystem Grants
2020-06-29 | NASA | A Semantics-Based Verification Toolset for UAS Embedded Software
2020-05-24 | Top 10 Blockchain Security and Smart Contract Audit Companies
2020-04-20 | Uniswap | Uniswap V2 Audit Report
2020-03-09 | CryptoNinjas | Runtime Verification enters a protocol verification agreement with PlatON blockchain
2020-03-09 | PlatON Networks | Runtime Verification Enters a Protocol Verification Agreement with PlatON
2020-02-04 | Ethereum Blog | Audit and formal verification of deposit contract bytecode completed by Runtime Verification
2020-02-03 | ETA | Runtime Verification joins Ethereum Trust Alliance (ETA) as a founding partner
2020-01-29 | 6 Best Smart Contract Auditors For Blockchain Platforms
2019-09-10 | Tezos Foundation | Announcing Second Cohort of Tezos Ecosystem Grants
2019-08-17 | Web3 Foundation | Web3 Foundation Grants — Wave 3 Recipients
2019-07-14 | Elrond Network | Elrond Initiates Cooperation With Runtime Verification — A Research and Development Company Specializing in Formal Methods
2019-06-25 | Algorand | Runtime Verification Formally Verifies the Algorand Blockchain Will Never Fork
2019-05-21 | Ethereum Foundation | Ethereum Foundation Spring 2019 Update
2019-05-05 | Waves | Mathematically proven 100% safe smart contracts
2019-04-27 | Week in Ethereum News | Gnosis Safe gets formally verified by Runtime Verification
2019-04-26 | Gnosis | Formal Verification— A Journey Deep into the Gnosis Safe Smart Contracts
2019-04-23 | UIUC CS News | Bootstrapping in Chicago
2019-04-03 | Panvala | Batch Two Token Grant Applications
2019-03-27 | Elrond Network | Welcoming Grigore Rosu as Advisor to Elrond
2019-01-04 | UIUC Research Park | EnterpriseWorks Graduate Runtime Verification Thrives in Urbana
2019-01-03 | Chicago INNO | Meet the IL Startup Helping NASA and Boeing Detect Errors in Their Software
2018-11-30 | Gnosis | Formal Verification of the Gnosis Safe Contracts
2018-10-18 | Bitrates | MakerDAO: A Stability Engine With a Decentralized Governance Model
2018-10-12 | Uniswap | Lightweight Formal Verification of Uniswap Smart Contract
2018-09-17 | MakerDAO | The Code is Ready
2018-08-22 | MakerDAO | Update on Availability of Multi-Collateral Dai
2018-08-21 | CASA | Storing your Ethereum Safely
2018-08-09 | Week in Ethereum News | Runtime Verification: how formal verification of smart contracts works
2018-08-01 | Cardano Forum | Webcast with Grigore Roșu, CEO of Runtime Verification
2018-07-31 | BC Focus | IOHK launches Cardano smart contracts testnet for IELE virtual machine
2018-07-31 | Crypto Ground | IOHK Launches Second Cardano Smart Contracts Testnet 'IELE'
2018-07-30 | Payment Week | IOHK Launches IELE Virtual Machine Testnet for Cardano Blockchain
2018-06-14 | Blokt | Cardano Brings Forward Its First Smart Contracts
2018-06-12 | Crypto News Monitor | Grigore Rosu: The K framework – a framework to formally define all programming languages
2018-06-07 | Bitrates | IOHK: Virtual Machines and Contract Code Correctness
2018-06-05 | invest in blockchain | Cardano Launches KEVM Testnet: What This Means and Why This is a Big Deal
2018-05-28 | IOHK | First Cardano smart contracts testnet launches
2018-03-07 | Ethereum Foundation | Announcing Beneficiaries of the Ethereum Foundation Grants
2017-12-20 | All Coins News | Virtual Machine for Blockchain Launched by Runtime Verification and IOHK
2017-12-20 | Chain Finance | Virtual Machine for Blockchain Launched by Runtime Verification and IOHK
2017-12-18 | Payment Week | Runtime Verification and IOHK Launch Virtual Machine for Blockchains
2017-12-18 | Payments Journal | Runtime Verification and IOHK Launch Virtual Machine for Blockchains
2017-12-18 | UIUC CS News | Runtime Verification and IOHK Launch Virtual Machine for Blockchains
2017-10-03 | UIUC CS News | Student uses a tool called K to build a path towards more secure blockchains
2017-10-02 | Crypto Ninjas | Research project produces first complete formal semantics of the Ethereum Virtual Machine
2017-08-02 | Econo Times | IOHK’s UIUC project builds formal semantics of Ethereum Virtual Machine
2017-08-02 | Coin Journal | KEVM Wins IC3-Ethereum Crypto Boot Camp 2017 Competition
2017-08-01 | Coinspeaker | IOHK-Funded UIUC Project Produces First Complete Formal Semantics of Ethereum Virtual Machine
2016-10-31 | UC San Diego | CSE Alumnus Wins Most Influential Paper for Work on Runtime Verification
2016-10-17 | UIUC CS News | Rosu earns ASE Most Influential Paper award for work that helped launch runtime verification field