TBTL Security

Security through
formal reasoning.

Smart contract and zero-knowledge program audits. Built on formal methods expertise, not pattern libraries.

40+ years formal verification expertise

Visit security.tbtl.com →

WHAT WE AUDIT

Two domains, one method

Where conventional audits check code against catalogues of known bugs, we reason from first principles about how a system can fail at all.

Solidity / EVM

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, and more
  • ·Analysing ERC standard compliance

ZK / Noir

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

THE DIFFERENCE

We ask how systems can fail, not just what has failed before.

HOW MOST FIRMS WORK

  • Manual review against known vulnerability patterns
  • Pattern-matching against CVE databases
  • “Have we seen this bug before?”

HOW WE WORK

  • Formal reasoning from first principles
  • Systematic analysis of the system's own failure modes
  • “How can this system fail?”

Every finding is grounded in practical exploitability. We focus on real-world vulnerabilities, not theoretical ones.

THE METHOD

What formal methods actually do

Testing checks a system against a sample of inputs and hopes the sample is representative. Formal methods build a mathematical model of the system and reason about every state it can reach. That's the difference between recognising a bug that's been seen before and anticipating one that hasn't.

01

Model

Translate the contract or program into a form a solver can reason about, capturing every state it can reach, not a sample of them.

02

Specify

State the properties it must always hold, such as no reentrancy, no double-spend, correct rounding, or sound constraints.

03

Check

Verify the model against the specification, and produce a concrete counterexample when a property doesn't hold.

We've built our own tools for this: Solidifier, a bounded model checker for Solidity, and NAVe, our formal verifier for Noir zero-knowledge programs. Building NAVe led us to find and fix a soundness bug in cvc5, the SMT solver it depends on. It was a defect that could have undermined any ZK program checked against it.

None of this amounts to a proof that a system is correct, and we don't present it as one. A check is only as complete as the properties it's specified against. What it gives you is a systematic account of how a system can fail, in place of a best guess.

TBTL SECURITY

Full engagement scope, methodology, and past reports live on security.tbtl.com.

security.tbtl.com ↗