Security through
formal reasoning.
Smart contract and zero-knowledge program audits. Built on formal methods expertise, not pattern libraries.
Comprehensive security review
Two specialised disciplines.
Smart contract audit
Comprehensive analysis of Solidity contracts across DeFi protocols, token standards, bridges, and upgradeable systems.
- Formalising and analysing requirements
- Checking reentrancy, integer overflow, etc.
- Analysing ERC standard compliance
ZK program analysis
In-depth review of Noir programs — built on NAVe, our published open-source formal verifier for Noir programs.
- Formalising and analysing requirements
- Checking constraint soundness & completeness
- Analysing proving system assumptions & setup
We ask how systems can fail, not just what has failed before.
- Manual review against known vulnerability patterns
- Pattern-matching against CVE databases
- "Have we seen this bug before?"
- Formal reasoning from first principles
- Systematic analysis of all possible failure modes
- "How can this system fail?"
The audit practice is a product of our research.
Solidifier: A bounded model checker for Solidity
A bounded model checker for Solidity that finds arbitrary bad states, not just known vulnerability patterns. Translates contracts into Boogie for analysis using the Corral solver.
Read paper →Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts
A framework requiring that contracts and any subsequent upgrades conform to a formal specification. Addresses safe upgradeability across ERC20, ERC3156, ERC1155, and ERC721 standards.
Read paper →NAVe: Formally Verifying Noir Zero Knowledge Programs
Formalises ACIR using SMT-LIB and the theory of finite fields, verified using the cvc5 SMT solver. The direct research foundation for our Noir audit capability.
Read paper →A Soundness Bug in cvc5’s Finite Field Split Solver
Our team at TBTL has discovered and fixed a bug in cvc5's finite-field split solver while testing our formal verifier NAVe. This bug could have undermined ZK programs and the ZK ecosystem.
Read post →Academic excellence applied to Web3 security.
Decades of formal methods and system security research, applied to the challenges of Web3.
Team Lead, Senior Research Scientist
Pedro Antonino
Oxford DPhil in Formal Verification. Author of NAVe, Solidifier, and Specification is Law. Affiliated with the Oxford Blockchain Research Centre.
Founder, TBTL · Advisor
Bill Roscoe
Former Head of Department, Oxford Computer Science. One of the most cited researchers in formal methods and concurrency theory. Author of The Theory and Practice of Concurrency.
Advisor
Srdjan Čapkun
Full professor at ETH Zürich. Leading researcher in system security and applied cryptography, spanning wireless security, trusted execution environments, and secure positioning.
Part of a broader security and research organisation.
The security division sits within TBTL (The Blockhouse Technology Ltd), a deep-tech company. TBTL also develops FortID, a full EUDI-compliant digital identity suite used by enterprises and governments navigating eIDAS 2.0, as well as Web3 components and consulting.
Ready to talk about your audit?
Tell us about your protocol, timeline, and scope. We will get back to you within one business day.