Est. 2010 · Formal Methods
We love formal methods
Runtime Verification has been proving code correct since 2010, spun out of the University of Illinois at Urbana-Champaign. We have worked alongside NASA and Toyota and grown into a trusted partner for organizations that develop software that cannot fail. Our tooling brings the highest level of rigor directly to software developers' hands. Based on the mathematical correctness of the K Framework our tools like Kontrol give a familiar property-testing based interface to developers and agents alike.
But most of all, we love formal methods. With a team from the world's top universities and deep expertise in system modeling, our approach is purpose-built for an age where AI writes more code than humans. Knowing what code should do, and proving it does, is our bread and butter.
Our approach
We're built different
The people
Meet the team
25+ senior engineers from the world's top universities. Low turnover, high depth.
Where we came from
Our history
From a university research group to a global security firm — the story of Runtime Verification.
Founded by Grigore Rosu
Grigore Rosu founds RV at the University of Illinois at Urbana-Champaign, where he pioneered formal disciplines.
OriginsFounded by Grigore Rosu
Grigore Rosu founds RV at the University of Illinois at Urbana-Champaign, where he pioneered formal disciplines.
OriginsThe K Framework goes public
We release the K Framework, a rewrite-based semantic framework for defining programming languages and their tooling.
ToolsThe K Framework goes public
We release the K Framework, a rewrite-based semantic framework for defining programming languages and their tooling.
ToolsFormal methods meets blockchain
We formalized EVM semantics in K (KEVM), helping pioneer formal verification for blockchain systems at a time when most security reviews relied entirely on manual auditing.
BlockchainFormal methods meets blockchain
We formalized EVM semantics in K (KEVM), helping pioneer formal verification for blockchain systems at a time when most security reviews relied entirely on manual auditing.
BlockchainMatching logic: a new foundation
Grigore Rosu publishes matching logic, a unifying foundation for program verification. It underpins our symbolic execution tools and lets us reason about language semantics and program correctness within a single framework.
ResearchMatching logic: a new foundation
Grigore Rosu publishes matching logic, a unifying foundation for program verification. It underpins our symbolic execution tools and lets us reason about language semantics and program correctness within a single framework.
ResearchSymbolic execution for modern software
We bring symbolic execution into modern development workflows, making formal analysis practical for real-world systems written in Rust, WebAssembly, Solidity, and beyond.
ProductSymbolic execution for modern software
We bring symbolic execution into modern development workflows, making formal analysis practical for real-world systems written in Rust, WebAssembly, Solidity, and beyond.
ProductSecurity for the AI age
25+ engineers from the world's top universities. AI writes more code than ever, which means the demand for people who can prove it works has never been higher.
NowSecurity for the AI age
25+ engineers from the world's top universities. AI writes more code than ever, which means the demand for people who can prove it works has never been higher.
Now