FVjobs

A job board for formal verification: proof assistants, automated reasoning, verified compilation, hardware verification, and the growing set of roles where AI writes proofs and something has to check them.

Browse the board at typetheoryforall.github.io/FVjobs, with search and filters for the kind of verification (hardware, software, AI for proof and autoformalization, academic, cryptocurrency), proof stack, remote work and employer size.

Maintained alongside Type Theory Forall.

Why this exists

Formal verification roles are scattered across company career pages, academic mailing lists and general job boards that have no idea what "Lean" means. This board collects them in one place and records the two things those boards never tell you up front:

• which proof stack the job actually uses — Lean, Rocq, Isabelle, SMT, SystemVerilog, F*, K;
• whether you can take the job — some roles are closed to anyone who is not a US person, some sponsor visas, and some are open worldwide.

Every entry carries the date someone last checked that the posting was live.

The data

data/jobs.yml is the source of truth; the site and its jobs.json are built from it. Besides the proof stack and work authorization, each entry records the kind of verification, location and remote policy, seniority, published pay, the date the employer posted it, and the date someone last checked it was live.

Closed roles move to data/archive.yml rather than being deleted: knowing that a company was hiring for Lean work six months ago is useful even when the posting is gone.

Adding a job

Open a new job issue — it is a short form, and no Git required. If you would rather send a pull request, add an entry to data/jobs.yml and run:

pip install pyyaml jsonschema
python3 scripts/validate.py --assign-ids

Leave id out of the new entry; --assign-ids gives it the next FV- number.

To preview the site locally, run python3 scripts/site.py and serve _site/.

See CONTRIBUTING.md for what belongs here and what does not.

Scope

In scope: roles whose core work is formal verification or closely supports it — proof engineering, automated reasoning, verified compilation, hardware formal verification, program analysis built on formal semantics, and AI-for-proof work.

Out of scope: general compiler and systems roles with no verification content, "security engineer" roles that are really appsec, and anything where the connection to formal methods is aspirational.

Licence

Code (the scripts) is MIT, see LICENSE. The job data in data/ is released under CC0 1.0 — take it, mirror it, build on it. See DATA-LICENSE.md.