SERVICES
What we audit
TBTL offers security analysis for two specialised domains: Solidity and EVM smart contracts, and zero-knowledge programs written in Noir, both grounded in formal methods research.
Smart contract audits
Formal methods-driven security analysis for DeFi protocols, token contracts, bridges, and on-chain infrastructure. Built on published research including Solidifier, our bounded model checker for Solidity.
- Formalising and analysing requirements
- Checking reentrancy, integer overflow, etc.
- Analysing ERC standard compliance
ZK program analysis
Formal analysis of zero-knowledge applications built with Noir. Grounded in NAVe, our SMT-checker-powered formal verifier for Noir.
- Formalising and analysing requirements
- Constraint soundness and completeness
- Analysing proving system assumptions and setup