About the role
You make the most important guarantees precise enough to check, focusing formal reasoning on the boundaries where a mistake is expensive. The honest version of this role includes being clear about the gap between a proved model, the code generated from it, and the environment it actually runs in.
The work
Model authorization, recovery, concurrency and distributed task state. Use model checking, proof assistants or program analysis where they add practical assurance. Work with engineers to connect specifications to implementations and make assumptions visible.
What good looks like
In your first 90 days, formalize one critical protocol, identify counterexamples or prove scoped properties, and add implementation checks.
Evidence we look for
Bring formal-methods expertise with an interest in shipping systems. Explain the relationship between a proved model, generated code and the actual deployed environment.
What we need to see
- Formal-methods expertise with a genuine interest in shipping systems
- You can explain the relationship between a proved model, the generated code, and the deployed environment
- You choose where formality pays for itself rather than trying to verify everything
- You can work with engineers who do not share your background
Nice to have
- TLA+, Coq, Lean, Dafny, or comparable in production use
- Verified cryptographic implementations
- You have found a real bug with a formal method
The exercise
Model revocation during failover and identify conditions under which a stale worker could still act.
Where and how we work
In the office together five days a week, in any of these cities. Remote-friendly around your family, arranged one person at a time.