Founded by Grigore Rosu
Grigore Rosu founds RV at the University of Illinois at Urbana-Champaign, where he pioneered formal disciplines.
OriginsEst. 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.
- 2010
- Founded
- 25+
- Senior engineers
- 3+ yrs
- Avg. team tenure
- 100+
- Security engagements
The people
Meet the team.
25+ senior engineers from the world's top universities. Low turnover, high depth.
Leadership
Team
Where we came from
Our history.
From a university research group to a global security firm: the story of Runtime Verification.
2010 2014 The K Framework goes public
We release the K Framework, a rewrite-based semantic framework for defining programming languages and their tooling.
Tools2017 Formal 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.
Blockchain2019 Matching 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.
Research2023 Symbolic 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.
ProductToday Security 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
Bring us your hardest problem.
See formal methods in action.