Founded by Grigore Rosu
Origins
Grigore Rosu founds RV at the University of Illinois at Urbana-Champaign, where he pioneered formal disciplines.
Est. 2010 · Formal methods
We love formal methods
A Runtime Verification engagement is not a checkmark. Whether it is a full audit, a formal proof, a fuzzing campaign or a design review, it is an uncompromising end-to-end examination, and a mark of a security conscious team.
- 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.
- 2010Chapter 1
- 2014Chapter 2
The K Framework goes public
ToolsWe release the K Framework, a rewrite-based semantic framework for defining programming languages and their tooling.
- 2017Chapter 3
Formal methods meets blockchain
BlockchainWe 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.
- 2019Chapter 4
Matching logic: a new foundation
ResearchGrigore 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.
- 2023Chapter 5
Symbolic execution for modern software
ProductWe bring symbolic execution into modern development workflows, making formal analysis practical for real-world systems written in Rust, WebAssembly, Solidity, and beyond.
- TodayChapter 6
Security for the AI age
Now25+ 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.
Bring us your hardest problem
See formal methods in action.