Work with me

Focused help with a design question, a difficult specification, or your use of verification tools. We can review an approach, work through a counterexample, or decide where formal methods would be useful for your team.

• Specification idioms, modeling choices, and tool guidance for TLA⁺, Quint, and Lean
• Advice on protocol design, verification strategy, and testing
• Integration with AI tools
• Online calls or on-site meetings

I work alongside your team to improve its specification and verification capabilities. Using a protocol or specification relevant to your work, we practice modeling, stating properties, and interpreting verification results, so the team can continue independently.

• Exercises tailored to your team's experience and the systems you build
• Hands-on work with TLA⁺, Quint, or Lean, chosen for your goals
• Joint review of specifications, invariants, counterexamples, and proofs
• Reusable examples and practical next steps for applying the methods in your daily work

A focused project to write, review, or strengthen a protocol specification. I work from design documents, existing models, or implementation code to clarify behavior, identify the properties that matter, and check the design before it reaches production.

• Executable specifications in TLA⁺ or Quint, including work from Rust, Go, or Solidity implementations
• Safety invariants, liveness properties, simulation, and model checking
• Speeding-up specification and verification with AI tools
• A findings report and handover of specifications your team can maintain

A collaboration for questions that need investigation as well as implementation. I work with your team to explore protocol designs, develop verification methods, and build tools that connect formal models to real systems.

• Protocol models, proof development, and experimental prototypes
• Specification-driven testing harnesses, fuzzing, fault injection, and invariant checking
• AI-assisted test generation where useful, with human review of specifications and results
• Reproducible results, documented tools, and integration into your team's workflow