Formal methods job postings
What does demand for formal methods skills look like these days? Is it worth learning these tools for a job, and who would hire you? Real, current hiring concentrates in two places: large-company research labs hiring for Lean/Coq/TLA+ expertise, and defense/government contractors requiring US citizenship and clearance.
Job boards
Section titled “Job boards”LinkedIn ★★★ linkedin.com. The richest source: research-engineer and principal-level full-time roles, not freelance work. Search used.
Wellfound ★★★ wellfound.com. Current startup jobs asking for formal methods (Axiomise, Tangram Flex, an SMT-based compiler role). Jobs for employees, not freelance. Search used.
web3.career ★★ web3.career. Crypto job board with real formal verification roles at Nethermind and the Ethereum Foundation. Example.
cryptocurrencyjobs.co ★★ cryptocurrencyjobs.co. Crypto job board with the same Nethermind and Ethereum Foundation roles. Example.
JobStash ★ jobstash.xyz. Web3 job board with a Formal Verification tag; listings not checked in depth.
FlexJobs ☆☆☆ flexjobs.com. Nothing found.
RemoteOK ☆☆☆ remoteok.com. Nothing found.
We Work Remotely ☆☆☆ weworkremotely.com. Nothing found.
Postings
Section titled “Postings”Formal methods is the job
Section titled “Formal methods is the job”| Role | Tech stack |
|---|---|
| Applied Scientist, Automated Reasoning, AWS, $172K-$222K | Formal verification, SAT/SMT solving, theorem proving, model checking; Lean, Dafny, Isabelle, Rocq; OCaml, Haskell, Rust, Scala, Kotlin. PhD required. 47 matching postings on amazon.jobs, in many locations |
| Principal Engineer, Memory Safety and Agentic Modernization, Google Cloud, $307K-$427K | Lean, TLA+, Verus to prove code correct during a large C/C++-to-Rust migration of the virtualization stack; Rust, C, C++. Director+ level |
| Formal Methods Research Engineer, Oath Technologies, $250K-$385K | Lean (main), Coq, Isabelle, SMT solvers. On-site in Berkeley |
| Research Scientist, Verified Code Generation, Google DeepMind, $174K-$252K | Lean, Rocq or similar proof assistants, SMT solvers; formal semantics of real languages like C/C++ |
| Research Engineer, Formal Methods, Harmonic | Lean 4, Coq, Isabelle, Agda |
| Member of Technical Staff, AI-Driven Compilation, San Francisco Tensor Company, $275K-$315K | SMT solvers; formal correctness proofs that gate a reinforcement-learning search over compiler output |
| Principal Systems Engineer: Linux Kernel, Cedana AI, $140K-$180K | No tools named; the team cites past formal methods work. Remote US |
| Formal Methods / Formal Verification, Acceler8 Talent (recruiter, client not named), $150K-$350K | Not specified |
Formal methods is a large part of the job
Section titled “Formal methods is a large part of the job”| Role | Tech stack |
|---|---|
| Formal Verification Engineer, Harmonic | Lean, Coq, Isabelle, Agda; verifying customers’ production hardware and software with Harmonic’s Aristotle |
| Formal Methods Engineer, Sigil Logic (closed) | TLA+, Alloy |
| Software Engineer, Formal Methods, Beyond Tabs (closed) | Model checking, SAT/SMT, for smart contracts |
| Senior Principal Software Engineer, Oracle (closed) | TLA+ |
| Member of Technical Staff, Formal Verification, Architect Labs (closed) | TLA+, Lean, Coq |
| Research Scientist, Formal Methods, Riverside Research, $60K-$115K | Rocq, Lean, Isabelle, SMT solvers, PL theory, seL4, LLVM, CompCert, Rust. US citizenship, clearance-eligible |
| Research Scientist, Cryptography with Formal Methods, Riverside Research, $95K-$175K | Rocq, Lean, Isabelle/HOL, EasyCrypt, F*, CryptoVerif. US citizenship, clearance-eligible |
| Research Software Engineer, Formal Methods, RTX/BBN, $87K-$165K (Arlington, Cambridge) | Model checking, theorem proving, SAT/SMT, logic programming; Python, C/C++, Java. Top Secret clearance and US citizenship |
| Senior Software Engineer, Formal Verification, Category Labs, $180K-$250K | Not fully checked; fintech/crypto infrastructure |
| Senior Security Engineer, Research & Engineering, Trail of Bits | Reads Lean, Rocq, F*, Dafny or Verus proofs to find what a verified system’s proof does not cover; Python, C++, Rust. Systems like HACL*, EverCrypt, seL4, CompCert, CakeML |
Internships, graduate roles and roles not open now
Section titled “Internships, graduate roles and roles not open now”| Role | Tech stack |
|---|---|
| Formal Methods Research Intern, Riverside Research, $25-35/hr | Rocq, Lean, Rust, OCaml. US citizenship |
| 2027 PhD Graduate, Formal Verification, Johns Hopkins APL, $105K-$245K | TLA+, SPIN, CVC5, MathSAT |
| 2027 Formal Methods Researcher Graduate Intern, The Aerospace Corporation, $32-38/hr | No tools named; formal methods for self-healing real-time systems. Master’s/PhD, US citizenship and clearance |
| Thesis: Formal Methods vs. Traditional Tests, ABB Sweden (closed) | Not specified |
| Formal Verification Engineer, Nethermind, ~$90K-$120K (recurring, not open now) | Lean; formal methods for zkVMs (SP1, OpenVM), Ethereum smart contracts and ZK verifiers |
| Researcher/Engineer, Formal Verification, Ethereum Foundation (listing looks stale) | Formal verification of cryptographic protocols and their code |
Closed long ago
Section titled “Closed long ago”| Role | Tech stack |
|---|---|
| Principal Research Engineer, Formal Methods, Huawei Ireland | TLA+ |
| Rust Formal Verification Engineer, Hashlock | Rust; formal verification of smart contracts |
Contract and gig roles
Section titled “Contract and gig roles”Gig, contract and freelance work, not full-time employment. The strongest current demand is from AI-training platforms hiring Lean 4 experts to write and check proofs, not from classic freelance marketplaces.
| Relevance | Role | Tech stack |
|---|---|---|
| ★★★ | Mathematician / Formal Methods roles, Alignerr, $170-200/hr | Lean 4 and Mathlib, formalizing proofs. 135 open listings, recruiting country by country |
| ★★ | Formal Methods (Lean 4) Expert, Mercor, $95/hr (closed) | Lean 4 and Mathlib, Coq, Isabelle or Agda |
| ★ | Research Fellowship, Surge AI | Broad STEM; Lean 4 work known only from one fellow’s LinkedIn |
| ★ | Research Scientist, Formal Methods/Computational Science, AfterQuery Experts, $100-170/hr | Grading AI output in math and science, not formal methods engineering. PhD, 10+ years |
| ☆ | Formal Methods Developer, PeoplePerHour (2010) | Z notation; a student homework request |
| ☆ | Z specifications homework, Freelancer.com (2012) | Z notation, UML |
Also on the list of AI-training platforms, not checked in detail: Handshake AI.
The platforms these were found on are rated on Freelance marketplaces.