Smart contract audits informed by formal methods research.
For DeFi protocols, token contracts, bridges, and on-chain infrastructure.
The approach
Vulnerabilities in deployed contracts cannot be patched without migration. The Ethereum ecosystem has lost billions to exploits that a more rigorous analysis process would have surfaced. Most audit firms conduct manual code review against known vulnerability patterns. We bring a deeper analytical framework.
Our formal methods background shapes how we read your code. We do not just ask "have we seen this bug before?" We ask "how could this system fail?"
What we cover
- Formalisation and analysis of requirements
- Reentrancy and cross-function attack vectors
- ERC standard compliance and deviation
- Upgradeability patterns and storage collisions
- Economic attack vectors and incentive misalignment
- Oracle manipulation and price feed assumptions
- Bridge and cross-chain message handling
The research foundation
Our Solidity analysis draws on published work including Solidifier, a bounded model checker for Solidity that finds arbitrary bad states rather than matching against known CVE patterns, and Specification is Law, a framework for verifying that contracts and their upgrades conform to a formal specification.
How an engagement works
Scoping
We work with your team to define the codebase, trust model, and any known areas of concern.
Analysis
Formal reasoning, custom tooling, and manual expert review run in parallel.
Report
Severity-graded findings with remediation guidance, delivered to your team.
Remediation review
After fixes are applied, we verify each remediation and issue a final report.
Request an EVM audit
Tell us about your protocol, timeline, and scope. We will get back to you within one business day.