Distributed protocols, bridges, consensus, governance: wherever standard tooling runs out and teams need something built to fit.
Methodology writeups on open systems: worked examples of how the tooling comes together.
Extracting a formal specification from a real distributed system and using Apalache + AI-assisted harnesses to explore failures around leader election, TCP disconnects, persistence, and recovery.
Blogpost →Human-written specification and LLM-assisted harness generation for five real TFTP implementations to surface protocol-level bugs traditional fuzzers miss.
Blogpost →Helping you with specification idioms, best practices, and tool understanding. Brought to you by the author of Apalache and Quint.
A structured audit of your existing specs, from English prose to formal specifications to find ambiguity, missing invariants, and underspecified behavior before they hit production. I'm equally comfortable working with implementation code, whether it's Rust, Go, or Solidity.
Purpose-built harnesses that pair human-written protocol specifications with AI-driven conformance testing and counterexample generation. The specifications can be in TLA+, Quint, or *something else*
End-to-end specification and verification engagements, from pseudo-code to checked model to findings report, with the specs left in a state your team can maintain.
Paid work with client teams on production protocols.
Researcher-practitioner at the intersection of formal methods and real distributed systems. Past: Informal Systems, Interchain Foundation, Inria, TU Wien. Principal investigator and developer of Apalache, a symbolic model checker for TLA+. Author of Quint. Based in Vienna, Austria, works across EU hours with the US, UK, EU.
→ Full research record