Member of Technical Staff
Build the systems that let AI agents prove their own software correct — from proof-assistant infrastructure to RL environments for verification.
What you’ll do
You’ll join a small team building the environments and infrastructure that let frontier models produce verified software: code with a machine-checked proof that it does what the specification says. Concretely, in your first months you might
- extend
rocq-dove, our task-level specification generator, to a new source language or a new class of transformations; - design the grader that decides whether a model’s proof is honest — no admitted lemmas, no smuggled axioms, no universe tricks;
- build the harness that runs thousands of agent rollouts against a proof assistant and turns the results into a dense training signal;
- profile and fix the parts of the pipeline where a 2× speedup means an order of magnitude more verified code per day.
Everything ships. The lf-lean release was a verified translation of 1,276 statements, produced 350× faster than the human baseline; the tooling that made it possible is what you’d be working on next.
What we look for
- You’ve built something real with a proof assistant (Rocq, Lean, Isabelle, F*, Dafny) or a compiler, and you know where the sharp edges are.
- You’re comfortable with large systems: you can read a 100k-line codebase, find the load-bearing part, and change it without breaking the rest.
- You pick problems a few orders of magnitude bigger than the current state of the art, and you finish the last mile.
- You’d rather have a proof than a test suite, and you can explain to a skeptic why.
We don’t require a PhD, publications, or prior ML experience. We do require that you love software and want to make correctness cheap.
How we work
We’re a research lab that ships. Small team, short loops, real deployments: the correctness feedback we build is used by the models we train. We write things down, we review each other’s specifications as carefully as each other’s code, and we prefer density to decoration.
Compensation
Salary and generous equity, set by level. Full health, dental, and vision; relocation support to San Francisco if you want it.