AI systems and AI-assisted software engineering
Architecture and workflow guidance for AI systems and AI-assisted engineering, including model and deployment trade-offs (frontier APIs vs. local / open-weight) and reliability concerns.
Dr. Thomas Pani
Independent Technical Advisor for Software Systems
Hands-on technical consulting on software architecture, AI engineering, and distributed systems, with deep expertise in software reliability.
Expertise
Software reliability and advanced testing
Testing strategy for complex and stateful behavior using property-based testing, model-based testing, fuzzing, executable specifications, test oracles, and deterministic simulation.
Distributed systems and protocols
Design and review of distributed, protocol-driven, and stateful systems, including consensus, ledgers, payments, blockchains, smart contracts, control planes and reconciliation loops.
Formal verification and automated reasoning
Practical application of model checking, executable specifications, and proof-oriented methods using tools such as TLA+, Lean, Alloy, and related verification tooling.
Developer tooling and engineering workflows
Assessment and design of reliability and verification tooling, CI/test infrastructure, adoption paths, product maturity, build-vs-buy decisions, and workflows that fit engineering teams.
Technical assessment and independent review
Architecture review, reliability assessment, technical diligence, tooling and vendor evaluation, and security-oriented review for blockchain, smart contract, and protocol systems.
Selected work
Aztec Labs · Governance protocol verification
Formally modeled a stateful on-chain governance protocol before it became critical infrastructure. The work covered cross-contract behavior across voting rounds, upgrades, staking, slashing, permissions, execution paths, and time-dependent phases.
Checked 125 invariants and 992 verification conditions, combining executable specifications, model checking, SMT-based analysis, manual review, and LLM-assisted formalization.
Venture-capital investors · Technical diligence on software-reliability tooling
Assessed competitive differentiation, practical limits, product maturity, and adoption barriers in software-reliability tooling.
Ethereum Foundation · 3-slot finality consensus
Formal modeling and verification of accountability, a fundamental safety property, in Ethereum's 3-slot finality consensus design.
Cross-validated the model across TLA+/Apalache, Alloy, and CVC5 to reduce tool-specific risk.
Independent security review · Blockchain and protocol systems
Identified high- and medium-severity vulnerabilities across Solidity/EVM, Stellar, Algorand, and Cosmos protocols, including private competitive audit work for Sherlock, a Web3 security review platform.
Wiener Ball der Wissenschaften · Technical advisory (IT)
Long-running technical advisory role for the Vienna Ball of Sciences. Responsible for technical advice and oversight around the event's IT needs, including webshop and online payment systems.
Technical workshops · Software reliability tooling and workflows
Designed and delivered hands-on workshops on distributed-systems reliability with executable specifications and protocol fuzzing for technical audiences at DevConf and Protocol Berg.
Informal Systems · Apalache, Quint, and protocol reliability tooling
Contributed to Quint and Apalache tooling for TLA+-style executable specifications, simulation, symbolic model checking, and protocol reliability.
Built Apalache Cloud, a parallel batch-execution engine that delivered 10× speedups on protocol-verification workloads. Work included AWS, Python, Go, Scala, TLA+, and TypeScript.
Conducted security reviews and audits of Cosmos SDK and IBC components.
Google Research and Google Cloud · ML evaluation and automated reasoning tooling
At Google Research, contributed to ML pipeline tooling and authored large-scale on-device evaluation workflows for mobile ML models.
At Google Cloud, built an automated-reasoning tool for machine-health telemetry inconsistencies using C++ and Z3 SMT.
TU Wien and Wolfgang Pauli Institute · Formal methods research
Conducted PhD-level research in automated reasoning, concurrent-program verification, and complexity analysis.
- Developed an extension of Eldarica for verification of concurrent and parameterized shared-memory programs. Implementation in Scala.
- Developed Coachman for automated complexity analysis of concurrent shared-memory programs. Implementation in OCaml.
- Developed an AI-driven portfolio verifier for software verification workflows. Implementation in Python.
Teaching included programming languages, object-oriented programming, formal methods, software verification, and information design.
Advisory work
I am available for independent advisory, consulting, technical assessment, architecture review, and specialist implementation work. Engagements are scoped around the technical question, not packaged as products.
- Architecture and reliability review for complex software systems.
- AI systems architecture, AI-enabled software engineering, and evaluation strategy.
- Developer tooling, verification tooling, and internal engineering workflow assessment.
- Advanced testing strategy using property-based testing, model-based testing, fuzzing, and executable references.
- Distributed-system and protocol review, including state-machine, consensus, and failure-behavior questions.
- Security-oriented protocol review for blockchain, smart contract, and distributed-protocol systems.
- Technical diligence, expert briefings, workshops, and written assessments.
Experience and credentials
Experience
- 2024–now Independent technical advisor for software systems
- 2022–2023 Research Engineer, Informal Systems
- 2014–2021 Researcher, TU Wien & Wolfgang Pauli Institute
- 2019 PhD SWE Intern, Google Research
- 2018 PhD SWE Intern, Google Cloud
- 2011–2014 Teaching in IT, data processing, and statistics; Schule für Gesundheits- und Krankenpflege Tulln
- 2004–2009 Early industry internships; AGRANA, Siemens, and Raiffeisen Informatik
Education
- 2021 Dr. techn. / PhD
Computer Science, TU Wien - 2014 Dipl.-Ing. / MSc
Computer Science, TU Wien - 2007 Network Engineering, HTL Rennweg
Awards
- 2017, 2018 FMCAD Best Student Contribution
- 2014 Best Master's Thesis, TU Wien
- 2009–2011 Academic Excellence Scholarship, TU Wien
Training
- 2023 LEGO® Serious Play® Facilitator
Association of Master Trainers - 2022 Patterns for Self-Organizing Teams
The Hum - 2022 Coaching as Management Tool
Gabriele Fischer - 2021 Voice & Body Language Skills
Kate Montague - 2012 From Ideas to Presentation
McKinsey & Company - 2012 Graphic Recording Workshop
sideprojects.dk
Writing, open source, and speaking
Technical blog
Longer technical material on executable specifications, formal verification, model checking, fuzzing, model-based testing, and AI-assisted software reliability lives at blltprf.xyz.
Open source
Apalache, symbolic model checker for TLA+ and Quint specifications. Maintainer. Linux Foundation project.
Quint, executable TLA+-style specification tooling. Early development team at Informal Systems, including language design.
Workshops
Recent workshops include distributed-systems reliability with executable specifications at DevConf and hands-on protocol fuzzing at Protocol Berg.
Contact
For advisory work, technical assessment, speaking, or specialist implementation: hello@thpani.net.
Based in Vienna, Austria. Available across Europe and internationally.