AI systems architecture and strategic AI consulting
Architecture choices, evaluation workflows, local and open-weight model exploration, embeddings, multimodal systems, and the reliability of AI-assisted software engineering.
Dr. Thomas Pani
Independent Technical Advisor for Software Systems
Advice on software architecture, AI systems, reliability, developer tooling, advanced testing, and distributed systems. Strategic assessment, architecture review, specialist implementation, and technical workshops.
Expertise
Advanced testing and software reliability
Property-based testing, model-based testing, fuzzing, executable specifications, test oracles, deterministic simulation, and techniques for making difficult stateful behavior testable.
Distributed systems, protocols, and stateful software
Consensus, concurrency, blockchains, smart contracts, ledgers, control planes, reconciliation loops, payment and state workflows, and protocol risk. Typical questions involve ordering, retries, and failure handling.
Formal verification and automated reasoning
Model checking and proof-oriented methods with tools such as TLA+, Lean, and Alloy. Used selectively, where they add evidence or clarify engineering decisions.
Developer tooling and engineering workflows
Internal tools, verification tooling, CI/test infrastructure, adoption barriers, product maturity, build-vs-buy questions, and practical workflows that fit how engineering teams actually work.
Independent technical assessment
Architecture and reliability review, technical diligence, tooling/vendor assessment, protocol and security risk, and written analysis for technical and non-technical decision-makers.
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 notebook
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: office@thpani.net.
Based in Vienna, Austria. Available across Europe and internationally.