Make the most important system guarantees precise enough to check. You will focus formal reasoning on boundaries where mistakes are costly.
Not open yet: Research program
This work starts when that stage arrives, so there is no application to submit today and we will not pretend otherwise. What is written below is what the role is for and what would make somebody right for it, published early on purpose so you can decide whether it is worth watching.
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.
The milestone
In your first 90 days, formalize one critical protocol, identify counterexamples or prove scoped properties, and add implementation checks.
Evidence
Bring formal-methods expertise with an interest in shipping systems. Explain the relationship between a proved model, generated code and the actual deployed environment.
Evidence, not credentials. We are describing work you can point at, in whatever form it exists.
The exercise
Model revocation during failover and identify conditions under which a stale worker could still act.