- Formal methods trained PhD researchers
- In-house security and AI tooling development
- People-first skills, AI-enhanced results
- Low turnover team (avg tenure of 4 years)
PhD researchers, AI-enhanced
Learn more about our team
Our work
Assurance work by formal methods experts
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.
How we work with teams
Most engagements combine several of these. We scope the mix with you, based on what the system is and what failure would cost.
Security audits
An end-to-end review of a codebase, from architecture down to individual unsafe blocks, ending in a report your team keeps.
Formal verification
Mathematical proof that the code does what the specification says, for the properties where testing is not enough.
Fuzzing campaigns
Targeted harnesses built around your critical properties, yours to keep and re-run long after the engagement ends.
Design reviews
A read of the design before the code exists, catching the expensive mistakes while they are still cheap to fix.
Agentic guardrails
Your agents need to be aware of, and held to, your security policies. We help teams find secure ways to run them.
Data partnerships
Years of modelling, review and verification under established processes, as training data for high-quality engineering practice.
What every engagement includes
Request WorkInvariant-First Analysis
Before touching the code, we define the invariants: the properties that must always hold. This ensures we know exactly what correct behavior looks like from the start.
A Barrage of Rigorous Tools
We verify invariants with symbolic execution, fuzzing, and model checking, including our partner Almanax, covering attack surfaces traditional reviews miss.
Reports That Go Beyond Bugs
Our reports include documented invariants, system descriptions, and architecture notes: lasting documentation your team can reference long after the engagement.
OpSec Best Practices
Beyond bugs, we recommend operational security improvements (key management, deployment procedures, access controls), building security into every layer.
The most complete security work in the industry.
Learn more about our team
- Free infrastructure to run your campaigns
- Test coverage and easy-to-read reports
- Run your harness fuzzing anytime
- AI agents integration for continuous fuzzing
KaaS, your all-in-one place for fuzzing
Learn more about KaaS
9
Years of expertise
$100B+
Total Value Secured
100+
Clients Protected
22
Security Experts
Work We're Proud Of
From blockchain launches to aerospace systems: a sample of what we've secured.
M
Monad: Pre-Launch Security Clearance
Full pre-launch review of the Monad blockchain: architecture hardening, fuzzing harness improvements, and last-mile production checks before one of the most anticipated chain launches in recent memory.
January 2026
NASA: Mission-Critical Formal Verification
Three consecutive NASA SBIR grants. When the most rigorous engineering organization on Earth needs formal methods expertise, they call Runtime Verification.
SBIR Grant
ES
Espresso Systems: High-Value Staking Contracts
A precision audit of Espresso's Solidity staking contracts, protecting significant on-chain value with the same depth of rigor we bring to full-scale protocol reviews.
Solidity · Staking
Soroban VM: Smart Contract Runtime Security
Two months inside Stellar's Rust-based smart contract execution environment, covering architecture review, deep fuzzing, and line-by-line analysis of every unsafe code block before mainnet launch.
Rust · Infrastructure
W
WASMI: Interpreter-Level Hardening
Every system built on a WASM interpreter inherits its bugs. Our weeks-long review of WASMI uncovered crash vectors and execution inconsistencies that would have silently propagated to every application above it.
Rust · WASM
Solana Foundation: Token Standard Verification
Formal verification and audit of Solana's p-token and token wrap programs, foundational standards that underpin billions in on-chain value across one of the fastest blockchains in the world.
Rust · Formal Verification
Why Runtime Verification
Formal Methods: the Security Edge in the Age of AI
As AI generates more of the code, the question isn't just whether it works, but whether it's correct. Formal methods define the standard. Everything else gets checked against it.
- Reviewing critical software since 2017
- Nearly a decade of reviews across any language: Rust, Go, C++, Solidity, JavaScript, and more. Our formal specification approach means the language is never the barrier; understanding the system is.
- Trusted by Leaders Across Industries
- DARPA, NASA, Boeing, the Ethereum Foundation, Solana, and Stellar have trusted us with critical systems, spanning aerospace, defense, and frontier technology.
- Open-Source by Conviction
- We build in the open. We maintain the K Framework (a formal methods platform used by researchers worldwide) and contribute to the broader security ecosystem.
- AI-Ready Security Specifications
- The specs and invariants we produce are machine-readable artifacts. We help teams encode security guarantees that AI agents can enforce throughout the development lifecycle.
Where we go deep
Three domains with a decade of work behind them, each with its own account of how the verification is actually done.
Embedded systems
Software that ships inside hardware, where a fault is physical. Formal methods applied to automotive, aerospace and safety-critical control code.
Consensus protocols
Formal specifications of a protocol design and its properties, then mathematical proof that the design meets them. Casper and Algorand were both done this way.
Smart contracts
Semantics-based analysis and verification of on-chain code, built on the same K definitions the research side of the company maintains.
"We see a worrisome trend in the industry where timelines are a race to the bottom, and we are not willing to compromise. A Runtime Verification audit report is a stamp of approval from our team. It's also a signal to our client's users and community that security is a priority, not an afterthought."
Everett Hildenbrandt
CEO of Runtime Verification
Not ready for a full engagement yet?
Learn how a Design Review can help you ship more secure code in as little as one week.