Hey, I’m Thomas 👋
I help protocol teams find deep correctness bugs and ship systems that behave as intended — even under adversarial or surprising conditions.

📫 Contact: blltprf.xyz · webintake@blltprf.xyz · @audithare

🧰 What I Focus On

• 🔍 High-context code review & security analysis – where subtle invariants actually matter
• 🧪 Fuzzing & deterministic simulation – exploring behaviours your test suite never reaches
• 📐 Formal modeling & verification – checking protocol properties with TLA+, Quint, Alloy, SMT
• 🧭 Protocol correctness guidance – design reviews, modeling patterns, failure-mode analysis

🚂 Recent work

• 🔥 Aztec Governance Protocol: Formal Verification – formal specification + symbolic verification of 125 invariants across a multi-contract governance system · write-up
• Ethereum Foundation: 3-slot finality (3SF) – formal modeling & verification of accountability · repo
• Protocol fuzzing workshop @ Protocol Berg v2 · recording + repo
• Soroban smart contract audit – private audit with authentication / authorization focus · TBA
• Solarkraft – runtime verification for Soroban/Stellar smart contracts · repo
• Core team: Apalache – symbolic model checker for TLA+ & Quint · repo
• Quint – modern language & tooling for TLA+ specs · repo