Skip to content
View thpani's full-sized avatar
🦚
🦚

Organizations

@code-423n4 @sherlock-audit @apalache-mc @blltprf

Block or report thpani

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
thpani/README.md

Hey, I'm Thomas 👋

I help engineering teams find the failure modes their tests weren't designed to catch. The same technique used internally at AWS, Oracle, and Microsoft; made practical for teams building complex stateful systems (distributed protocols, cloud-native architectures, payment infrastructure) who need or already run fuzzers, chaos injection, or DST.

As AI-generated code reaches production faster than test suites can keep pace, executable specs are one of the few techniques that can keep up. They describe intent precisely enough to test generated code against, and can be invoked by agents as a verification tool at generation time.

Make complex software boring again.

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


What I Focus On

🎯 Test Oracle Design: if your team already runs fuzzers, DST, or property-based testing, I help you design a specification-based oracle that dramatically increases the signal from tools you already have
Model-Based Adversarial Testing: end-to-end: spec, adversarial test generation via random and symbolic execution, conformance testing against the implementation
🤖 AI-Generated Code Testing: executable specs as precise oracles for LLM-generated protocol code, invokable by agents at generation time
📐 Protocol Specification and Review: executable specs for critical components (distributed protocols, cloud-native architectures, payment infrastructure), including invariant writing, simulation, and model checking

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 – model-based runtime monitoring for Soroban/Stellar smart contracts · repo
  • Apalache – core team member; symbolic model checker for TLA+ & Quint · repo
  • Quint – modern language & tooling for TLA+ specs · repo

Pinned Loading

  1. fuzz-pb25 fuzz-pb25 Public

    Fuzzing Workshop at Protocol Berg Berlin, June 2025

    Python 3

  2. freespek/ssf-mc freespek/ssf-mc Public

    EF project Exploring Automatic Model-Checking of the Ethereum specification

    TeX 8

  3. freespek/solarkraft freespek/solarkraft Public

    Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

    TypeScript 12 1

  4. apalache-mc/apalache apalache-mc/apalache Public

    APALACHE: symbolic model checker for TLA+ and Quint

    Scala 549 48

  5. informalsystems/quint informalsystems/quint Public

    An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

    TypeScript 1.3k 126