Trust but verify.
High-assurance security audits and compliant digital identity, built on academic rigour.
Expertise in formal methods, decentralised systems, and trusted hardware, backed by peer-reviewed papers and granted patents.
01 · SECURITY PRACTICE
Security through formal reasoning.
Smart contract audits and zero-knowledge program analysis, built on formal methods expertise. We use formal reasoning to analyse how a system can fail.
Visit security.tbtl.com →02 · FORTID
Digital identity, without the exposure.
A production-ready, EUDI/eIDAS-compliant digital identity stack. It lets organisations verify who they're dealing with, without harvesting or exposing personal data.
Visit fortid.com →CORE TECHNOLOGIES
Three technologies behind our work
We research all three, and build on them across our products and services.
Formal Methods
Formal methods let us mathematically reason about everything a system could do, unlike testing methodologies that check it against a catalogue of expected behaviours. We use them to model smart contracts and ZK programs and to verify attestation protocols, building formal verifiers like Solidifier and NAVe along the way.
Use cases
- Formal analysis of smart contracts & ZK programs
- Verification of attestation and distributed protocols
System guarantees
Safety and liveness
Decentralised Systems
Decentralised systems are networks of independent nodes that must agree, recover from failure, and generate randomness without a central authority. We research and advise on consensus, checkpointing, and on-chain randomness, as well as blockchain components and protocols more generally.
Use cases
- Consensus and checkpointing protocol design
- Fault-tolerance system hardening
System guarantees
Availability and integrity
Trusted Hardware
Trusted Execution Environments (TEEs) isolate code and data so nothing outside them, not the cloud provider, the host operating system, or another process, can read what is inside. We use this isolation to protect signing keys in Cloud Wallet and Custody, and to harden systems. We also design and analyse attestation protocols.
Use cases
- Confidential data storage and processing
- TEE-based system hardening
System guarantees
Confidentiality and integrity
RESEARCH & PATENTS
Research grounded in practice
The papers behind the methods, and the patents behind the technology.
paper
Hierarchical Consensus: Scalability Through Optimism and Weak Liveness
Pedro Antonino, Antoine Durand, A. W. Roscoe
DISC · 2025
paper
Pedro Antonino, Antoine Durand, A. W. Roscoe
DISC · 2025
Consensus
A new approach to reaching agreement across a blockchain network without sacrificing liveness under partial synchrony.
Read paper ↗patent
Performing tasks in distributed computer systems
Roscoe, Antonino
GB2625227B · granted 2025
patent
Roscoe, Antonino
GB2625227B · granted 2025
Decentralised systems
A handover scheme for blockchain consensus: if one group of nodes can't reach a timely decision, a larger, more robust group takes over, without the two ever producing conflicting results.
View patent ↗paper
Hooks: A Simple and Modular Checkpointing Protocol for Blockchains
Pedro Antonino, Antoine Durand, Namrata Jain, Garry Lancaster, Jonathan Lawrence, A. W. Roscoe
IEEE NCA · 2024
paper
Pedro Antonino, Antoine Durand, Namrata Jain, Garry Lancaster, Jonathan Lawrence, A. W. Roscoe
IEEE NCA · 2024
Checkpointing
A modular protocol for recovering blockchain state after failure, designed to plug into existing systems rather than replace them.
Read paper ↗patent
Method and device for preventing forking of blockchain
Chen, Roscoe
US12,254,468 B2 · granted 2025
patent
Chen, Roscoe
US12,254,468 B2 · granted 2025
Decentralised systems
A backlinking method that lets a newly joined node work out which chain is the legitimate one, without needing to re-verify the network's entire history.
View patent ↗paper
Guardian: Symbolic Validation of Orderliness in SGX Enclaves
Pedro Antonino, Wojciech Aleksander Woloszyn, A. W. Roscoe
CCSW · 2021
paper
Pedro Antonino, Wojciech Aleksander Woloszyn, A. W. Roscoe
CCSW · 2021
Symbolic enclave analysis
A symbolic method for checking that code inside an SGX enclave executes operations in the order it claims to.
Read paper ↗patent
Storing Cryptographic Keys Securely
Capkun, Matijasevic, Novoselac
GB2611412B · granted 2023
patent
Capkun, Matijasevic, Novoselac
GB2611412B · granted 2023
Trusted hardware
Splits a key into independently generated components, each secret-shared across separate stores, so compromising some shares still isn't enough to reconstruct the key.
View patent ↗paper
Flexible Remote Attestation of Pre-SNP SEV VMs Using SGX Enclaves
Pedro Antonino, Ante Derek, Wojciech Aleksander Woloszyn
IEEE Access · 2023
paper
Pedro Antonino, Ante Derek, Wojciech Aleksander Woloszyn
IEEE Access · 2023
Attestation
A way to remotely verify the integrity of AMD SEV virtual machines using SGX enclaves, ahead of native SEV-SNP support.
Read paper ↗patent
Custody service for authorising transactions
Antonino, Derek, Hecimovic, Matijasevic, Novoselac, Vidakovic
GB2607282B · granted 2023
patent
Antonino, Derek, Hecimovic, Matijasevic, Novoselac, Vidakovic
GB2607282B · granted 2023
Trusted hardware
A TEE-based custody server that holds a private key inside an enclave and signs a transaction only when the request satisfies a configurable access policy.
View patent ↗What we build and advise on
Cloud Wallet
TEE-secured custody and recovery for everyday digital asset transfers, with no seed phrase to lose.
Learn more →Custody
Institutional-grade custody secured across Trusted Execution Environments and multi-party computation.
Learn more →Blockchain Consulting
Advisory on consensus, checkpointing, and on-chain randomness protocols, grounded in our own research.
Learn more →TEE Consulting
Hardening TEE-based systems and verifying the attestation protocols that prove what's running inside them.
Learn more →TBTL SECURITY
Smart contract and ZK/Noir audits, covering the full division in depth.
security.tbtl.com ↗FORTID, BY TBTL
The EUDI/eIDAS-compliant identity stack: products, docs and dev tools.
fortid.com ↗Working on a system you can't afford to get wrong?
Book a call to discuss your concerns, and we'll explore how we can help.