Jobs in 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. Each entry says which proof stack the job uses, whether you can take it from where you live, and when someone last checked that it was open.

140 open roles at 81 companies. Maintained alongside Type Theory Forall.

Access Softek Toolchains Software

Compiler Developer (LLVM, C++)

Remote (worldwide) Anywhere

Engineer
- LLVM
- Clang
- C++
- compilers
- toolchains
Posted 2019-11-18
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
No restriction stated; "work from anywhere in the world"
AdaCore Software

Internship - SPARK: Formally verify an ordered set/map library in SPARK

On-site Toulouse, France

Intern
- SPARK
- Ada
- safety-critical software
- verified libraries
Checked 2026-10-27

Pay, eligibility and notes
Notes
Six months during 2027. Proves the absence of runtime errors and more in SPARKlib's red-black-tree containers, with AI-assisted proof.
Advanced Micro Devices (AMD) Hardware

CPU Formal Verification Engineer

On-site Cambridge, United Kingdom

Senior
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- hardware
- CPU
Posted 2026-07-16
Checked 2026-10-27

Pay, eligibility and notes
Notes
CPU IP formal methodology, FPV/X-prop/DPV/SEC apps. The scope includes exploring formalisation of the ISA and memory models.
Advanced Micro Devices (AMD) Hardware

Lead Formal Verification Engineer

On-site Austin, TX / Orlando, FL / San Diego, CA

Lead
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- Murphi
- theorem proving
- hardware
- GPU
Posted 2026-10-09
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 175,000–250,000 base (range in AMD careers listing data; not rendered as prose)
Work authorization
Not eligible for visa sponsorship (stated in posting)
Notes
Sets formal strategy for AMD graphics/GPU IP, including datapath, equivalence and security verification.
Advanced Micro Devices (AMD) Hardware

Staff Formal Verification Engineer (GPU)

Hybrid Cambridge, United Kingdom

Lead
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- Murphi
- theorem proving
- hardware
- GPU
Posted 2026-06-18
Checked 2026-10-27

Pay, eligibility and notes
Notes
Primary point of contact for formal across AMD's graphics IP. The scope includes exploring formalisation of the GPU ISA and memory model.
Airbus Software

STAGE 2027 Formalisation pour la spécification et l'architecture logicielle

On-site Toulouse, France

Intern
- Rocq
- F*
- Lean
- Idris
- AADL
- SysML
- avionics
- aerospace
Posted 2026-09-24
Checked 2026-10-27

Pay, eligibility and notes
Notes
Six months starting around March 2027, in the Avionics Software department (flight controls and related critical software).
Alignerr AI for proof & autoformalization

Lean 4 Proof Engineer - Mathematical Formalization

Remote (worldwide) Remote

Engineer
- Lean
- Coq
- Isabelle
- Agda
- AI for mathematics
- AI training data
Posted 2026-10-22
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 170–200/hour (hourly contract, 10–40 hours/week)
Notes
Freelance AI-training contract (Alignerr is Labelbox's expert network). Translate informal proofs into Lean 4 and document where automated provers fail. Asks for a Master's or higher in mathematics, logic or theoretical CS.
Amazon (Amazon Leo) Hardware

Sr. Formal Verification Engineer, Amazon Leo

On-site Austin, TX / Sunnyvale, CA / Redmond, WA / San Diego, CA

Senior
- SystemVerilog
- SVA
- JasperGold
- Questa Formal
- hardware
- satellite communications
Posted 2026-08-26
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 185,200–250,000 (Austin, San Diego, Redmond); USD 213,000–287,500 (Sunnyvale)
Work authorization
Export control: US citizen or national, US permanent resident, or admitted refugee/asylee required
Notes
Modem SoCs for the Amazon Leo (formerly Kuiper) LEO satellite constellation.
Amazon (Annapurna Labs) Hardware

ASIC Formal Verification Engineer I, Annapurna Labs

On-site Austin, TX / Cupertino, CA

Engineer
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- hardware
- AI accelerators
Posted 2026-10-22
Checked 2026-10-27

Pay, eligibility and notes
Pay
Listed base: USD 116,100 (Austin) / USD 133,600 (Cupertino) annually
Notes
New-grad role on the Machine Learning Acceleration (Trainium/Inferentia) team; coursework or internship in formal methods required.
Amazon (Annapurna Labs) Hardware

Senior Formal Verification Engineer, Annapurna Labs

On-site Haifa, Israel

Lead
- SystemVerilog
- SVA
- hardware
- CPU
- cloud
Posted 2026-10-19
Checked 2026-10-27

Pay, eligibility and notes
Notes
L6 technical lead owning FV strategy for a Graviton/Nitro subsystem; team includes AI/agentic formal flows.
Amazon Web Services Software

2027 Applied Science Internship - Automated Reasoning - United States, PhD Student Science Recruiting

On-site Seattle, WA

Intern
- SAT
- SMT
- theorem proving
- model checking
- Lean
- cloud
- AI safety
Posted 2026-09-17
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 135,660 annualized (Seattle)
Work authorization
US internship; must be enrolled in a PhD and able to relocate
Notes
Minimum 12 weeks at 40 hours/week.
Amazon Web Services Software

Applied Scientist, Amazon Cryptographic Libraries

On-site Seattle, WA

Research scientist
- HOL Light
- Isabelle/HOL
- Lean
- Rocq
- Verus
- cryptography
- post-quantum cryptography
Posted 2026-08-31
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 142,800–193,200
Work authorization
US-based; sponsorship not stated
Notes
Machine-checked proofs of AWS-LC's C and assembly, including ML-KEM, ML-DSA and SLH-DSA. Early-career, with mentoring from senior scientists. A twin requisition, 10524924, has identical text.
Amazon Web Services Software

Applied Scientist, Automated Reasoning

On-site Multiple US cities

Research scientist
- Lean
- Rocq
- Dafny
- Isabelle
- SMT
- cloud
- cryptography
- AI safety
Posted 2026-08-14
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 167,100–260,000 depending on location
Work authorization
US-based; sponsorship not stated
Notes
Requires a PhD or equivalent research experience.
Amazon Web Services Software

Principal Applied Scientist, Neuro-Symbolic AI Labs

On-site Boston, MA

Principal
- proof assistants
- AI for reasoning
- AI for mathematics
Posted 2026-04-27
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 198,900–269,000
Work authorization
US-based; sponsorship not stated
Notes
Team includes an Amazon Scholar in mathematics and collaborates with MIT, Berkeley and CMU.
Amazon Web Services AI for proof & autoformalization

Senior Applied Scientist, AWS Quick

On-site Santa Clara, CA

Senior
- SMT
- model checking
- Lean
- automated reasoning
- AI safety
- generative AI guardrails
Posted 2026-05-22
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 192,200–260,000 (Santa Clara)
Notes
Neuro-symbolic team behind Automated Reasoning checks. Builds formal reasoning into GenAI and agent products for hallucination detection, policy verification and guardrails. Different team from the Automated Reasoning Applied Scientist role already on the board.
Amazon Web Services Software

Senior Applied Scientist, Neuro-Symbolic AI Labs

On-site Boston, MA / Santa Clara, CA

Senior
- proof assistants
- Lean
- Dafny
- AI for reasoning
- AI for mathematics
Posted 2026-08-18
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 167,100–226,100 (Boston); USD 192,200–260,000 (Santa Clara)
Work authorization
US-based; sponsorship not stated
Notes
A twin requisition, 10503196, has identical text.
Amazon Web Services Software

Sr Applied Scientist, Amazon Cryptographic Libraries

On-site Seattle, WA

Senior
- HOL Light
- Verus
- CBMC
- Lean
- cryptography
- post-quantum cryptography
Posted 2026-08-31
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 167,100–226,100
Work authorization
US-based; sponsorship not stated
Notes
Senior version of the AWS-LC proof role; Rust, C and assembly verification with AI-assisted proof development. A twin requisition, 10524925, has identical text.
Amazon Web Services Software

Sr. Applied Scientist, Automated Reasoning in Identity

On-site Santa Clara, CA

Senior
- SAT
- SMT
- BDDs
- theorem proving
- model checking
- cloud
- identity and access management
Posted 2026-08-31
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 192,200–260,000
Work authorization
US-based; sponsorship not stated
Notes
Builds tools that prove the absence of security problems in customer IAM configurations; PhD or equivalent research experience required.
Amazon Web Services Software

Sr. Software Development Engineer, Automated Reasoning Group

On-site New York, NY

Senior
- automated reasoning
- formal methods
- AI safety
- cloud
Posted 2026-07-15
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 184,900–250,200
Work authorization
US-based; sponsorship not stated
Notes
Builds Automated Reasoning Checks (ARc), which uses logic to verify generative-AI outputs. Formal methods experience is preferred, not required.
Antithesis Software

Senior/Staff Engineer - Bombadil

On-site London, UK

Senior
- LTL
- property-based testing
- Rust
- testing
- web applications
Posted 2026-03-18
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
No visa sponsorship; must already be authorized to work in the UK
Notes
Maintains Bombadil, Antithesis's open-source specification language and verifier for web UIs.
Apple Hardware

Formal Verification Engineer

On-site Austin, TX / Beaverton, OR / Cupertino, CA

Engineer
- SystemVerilog
- SVA
- hardware
- security
Posted 2026-04-13
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 115,773–194,700 base (Cupertino range)
Notes
Entry-level (0 years required). The role focuses on the Secure Enclave and security-requirement verification.
Apple Hardware

Formal Verification Engineer

On-site Munich, Germany

Various
- SVA
- PSL
- hardware
- CPU
Posted 2026-09-24
Checked 2026-10-27

Pay, eligibility and notes
Notes
Posting says Apple is hiring all levels from junior to senior; description reads as a formal verification architect role.
Apple Hardware

GPU Formal Verification Engineer

On-site Santa Clara, CA

Engineer
- SystemVerilog
- SVA
- hardware
- GPU
- security
Posted 2026-10-26
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 150,400–277,600 base
Notes
Apple Silicon formal team. The work covers formal micro-architecture specifications and security-attack modelling.
Arizona State University Academic

Professor (all ranks) in Verification, Validation, and Certification of AI-Enabled Complex Dynamical and Cyber-Physical Systems

On-site Tempe, AZ, USA

Lead
- formal verification of hybrid systems
- runtime assurance
- cyber-physical systems
- autonomy
- AI safety
Checked 2026-10-27

Pay, eligibility and notes
Notes
Faculty position (tenure-track or tenured, any rank), start August 2027. Deadline 2026-11-30; later applications go to a reserve pool.
Arm Hardware

Formal Verification Engineer

Hybrid Cambridge, United Kingdom

Senior
- model checking
- SystemVerilog
- hardware
- CPU
Posted 2026-09-16
Checked 2026-10-27

Pay, eligibility and notes
Pay
GBP 55,300–74,800
Notes
Solutions Group. The posting asks for assume-guarantee reasoning, invariants and abstraction skills.
Arm Hardware

Staff Architecture Formal Engineer

Hybrid Cambridge, United Kingdom

Senior
- OCaml
- ASL
- memory model tools
- hardware
- ISA specification
Posted 2026-06-25
Checked 2026-10-27

Pay, eligibility and notes
Pay
GBP 97,300–131,700
Work authorization
UK skilled worker sponsorship available; Arm covers employer-side costs only; no relocation package
Notes
Architecture Formal Team, which works on the Arm concurrency model and a formal description of ASL (the language of the Arm ARM). Builds lightweight verification tools.
Arm Hardware

Theorem Proving Engineer

Hybrid Austin, TX

Research engineer
- ACL2
- SLEC
- C
- Verilog
- hardware
- CPU
- floating point
Posted 2026-07-09
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 198,100–268,000
Notes
Datapath RTL is proved equivalent to C models (SLEC), and the C models are proved correct against the architecture spec in ACL2. Requires an MS or PhD in CS or Mathematics.
Astera Labs Hardware

Distinguished Formal Verification

On-site San Jose, CA

Principal
- SystemVerilog
- SVA
- hardware
- interconnect
- AI infrastructure
Posted 2026-02-23
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 230,000–285,000
Notes
Company-wide technical authority on formal for PCIe/CXL/Ethernet/UCIe/UALink products.
Astera Labs Hardware

Formal Verification and RTL Design Software Engineer

On-site San Jose, CA

Senior
- JasperGold
- VC Formal
- SystemVerilog Assertions
- Python
- LLM agents
- hardware
- AI for chip design
Posted 2026-08-31
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 160,500–200,000
Notes
AppliedAI team building LLM agents for formal proof convergence, lint and static verification flows.
Astera Labs Hardware

Senior/ Staff Formal Verification Engineer

On-site Tel Aviv, Israel

Senior
- SystemVerilog
- SVA
- hardware
- interconnect
- AI infrastructure
Posted 2026-03-18
Checked 2026-10-27

Pay, eligibility and notes
Notes
Founding member of Astera's new Israel R&D centre; owns formal environments from scratch to sign-off.
Astera Labs Hardware

Tech Lead, Formal Verification

On-site Bengaluru, India

Lead
- SystemVerilog
- SVA
- hardware
- interconnect
- AI infrastructure
Posted 2026-08-03
Checked 2026-10-27
Axiom Math AI for proof & autoformalization

Member of Technical Staff

Remote Palo Alto, CA / London, UK / Portland, OR / US remote / UK remote

Research scientist
- Lean
- Coq
- Isabelle
- AI for mathematics
- theorem proving
Posted 2026-04-03
Checked 2026-10-27

Pay, eligibility and notes
Notes
AI for mathematical discovery (successors to PatternBoost). Wants large-scale RL and neuro-symbolic experience plus a strong foundation in formal proof systems. Axiom makes AxiomProver and is moving into verified code generation.
Axiomise Hardware

Graduate Formal Verification Engineer

On-site Hemel Hempstead, United Kingdom

Engineer
- SystemVerilog
- SVA
- PSL
- hardware
- EDA services
Posted 2026-01-08
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
For recent UK-based graduates; Graduate-visa holders sponsored for a Skilled Worker visa after the programme
Notes
The graduate programme cohort starts in 2026.
Axiomise Hardware

Senior Formal Verification Engineer

On-site Hemel Hempstead, United Kingdom

Senior
- SystemVerilog
- SVA
- hardware
- EDA services
Posted 2026-04-20
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Visa sponsorship offered for exceptional candidates, on conditional terms
Notes
Includes line-management responsibilities.
Axiomise Hardware

Staff Formal Verification Engineer

On-site Hemel Hempstead, UK

Principal
- SystemVerilog Assertions
- PSL
- theorem proving
- equivalence checking
- hardware
- verification services
Posted 2026-04-20
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Visa sponsorship "for exceptional candidates"
Bedrock Robotics Software

2027 Internship Safety Engineer, Agentic Safety Case Assessment

On-site San Francisco, CA

Intern
- Lean
- Mathlib
- Aeneas
- Verus
- Kani
- robotics
- autonomous vehicles
- safety cases
Posted 2026-09-25
Checked 2026-10-27

Pay, eligibility and notes
Notes
Autonomous-excavator company. Intern formalises a safety claim, writes and proves a checker in Lean, runs it on fleet data, and builds audit tooling for LLM-assisted proving. Students only.
Beneficial AI Foundation Software

AI Safety Research Scientist / Research Engineer (formal verification)

Remote (worldwide) Anywhere

Various
- Lean
- Verus
- Rust
- AI safety
- cryptography
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 30–75/hour depending on role
Notes
Max Tegmark's foundation. Verifies production cryptographic Rust in Lean (curve25519-dalek, Signal protocols) — see github.com/Beneficial-AI-Foundation.
Cadence Design Systems Hardware

Software Engineer I: Jasper R&D

On-site Belo Horizonte, Brazil

Engineer
- Jasper
- C++
- EDA tools
Posted 2026-08-24
Checked 2026-10-27

Pay, eligibility and notes
Notes
Develops the Jasper formal tool itself, working on formal engines, HDL synthesis and graph modelling.
Cadence Design Systems Hardware

Software Engineer II

On-site Austin, TX

Engineer
- Conformal LEC
- C++
- EDA tools
Posted 2026-09-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Conformal team building the Conformal Logical Equivalence Checking, ECO and Low Power tools. The generic title hides the formal content.
Cajal AI for proof & autoformalization

Open applications (Lean, verified code)

On-site San Francisco, CA (from the YC profile; the careers page gives no location)

Various
- Lean
- WebAssembly
- verified code optimization
- scientific computing
Checked 2026-10-27

Pay, eligibility and notes
Notes
YC W26 company. Its product Tau optimizes hot routines and proves in Lean that each version behaves like the original. To apply, open a PR to Talos (their open-source Lean Wasm interpreter), then email careers@caj.al. They say they do not look at CVs.
CertiK Cryptocurrency

Software Engineer (III to Principal), Formal Methods

Remote New York / Seattle / SF Bay Area / Remote

Engineer
- SMT
- model checking
- OCaml
- Haskell
- blockchain
- smart contracts
Posted 2022-07-30
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 115,000–230,000 (US)
Notes
Wants model checking (BMC, CEGAR, IC3/PDR); publications at POPL/CAV/TACAS preferred.
CertiK Cryptocurrency

Solidity Compiler Frontend Engineer

Remote US / Remote

Engineer
- SMT
- theorem provers
- Solidity
- Java
- EVM
- blockchain
- smart contracts
- compilers
Posted 2025-10-20
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 140,000–220,000 (US)
Work authorization
US remote only ("US / Remote"); hires must complete US employment-eligibility verification; visa sponsorship not stated
Notes
Builds the Java-based Solidity compiler frontend (parsing, type checking, semantic analysis) and the layer that feeds CertiK's formal verification tools. Requires 3+ years of compiler work and experience with SMT solvers or theorem provers. Sits alongside CertiK's Formal Methods SWE role, which is already on the board.
CLEARSY Software

Ingénieur développeur full stack Atelier B H/F

Hybrid Aix-en-Provence, France

Engineer
- Atelier B
- B method
- C++
- Qt
- formal methods tooling
- railway
Checked 2026-10-27

Pay, eligibility and notes
Notes
Develops and modernises Atelier B (C/C++ back end, Qt front end). Published May 11, 2026.
CLEARSY Software

Ingénieur Méthodes Formelles H/F

Hybrid Aix-en-Provence, France (also Paris and Lyon)

Engineer
- B method
- Atelier B
- railway
- safety-critical systems
Posted 2026-08-17
Checked 2026-10-27

Pay, eligibility and notes
Pay
EUR 33,000–55,000 per year
Notes
Same posting in three cities: Paris https://clearsy.nos-recrutements.fr/job/5912 and Lyon https://clearsy.nos-recrutements.fr/job/5914. French-language posting; Bac+5 engineering profile. Teleworking agreement available.
CLEARSY Software

Ingénieur validation formelle de données sécuritaires H/F

Hybrid Aix-en-Provence, France

Engineer
- B method
- formal data validation
- railway
- safety-critical systems
Checked 2026-10-27

Pay, eligibility and notes
Notes
Long-running posting (published July 22, 2025) still listed; formal validation of safety constraints on railway project data.
Code Metal Software

Research Engineer — Formal Methods

Hybrid Boston, MA

Research engineer
- theorem proving
- SMT
- program synthesis
- static analysis
- compilers
- embedded
Posted 2026-05-22
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 180,000–266,800 plus equity
Work authorization
US Top Secret clearance eligibility listed as required
Cognichip Hardware

Formal Verification Engineer - AI

On-site Redwood City, CA / Toronto, ON

Engineer
- model checking
- Coq
- Lean
- Isabelle
- ACL2
- Z3
- cvc5
- hardware
- AI for chip design
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 175,000–210,000
Notes
AI-for-chip-design startup. Open to people from pure maths/physics; mentorship and structured ramp-up into formal methods offered. Listing also at cognichip.ai/careers.
Cornell University Academic

Postdoc in formal methods and programming languages (Alexandra Silva's group)

On-site Ithaca, NY, USA

Postdoc
- algebraic program analysis
- program repair
- networking
- security
- agentic systems
Posted 2026-10-12
Checked 2026-10-27

Pay, eligibility and notes
Notes
Announced on TYPES-announce on 2026-10-12. No deadline and no official ad; candidates are asked to contact the PI directly.
eleQtron Software

Compiler Engineer (m/w/d)

On-site Hamburg or Siegen, Germany

Engineer
- LLVM
- MLIR
- QIR
- C++
- Rust
- quantum
- compilers
Posted 2026-09-22
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Relocation support offered; EU Blue Card route for non-EU candidates
EPFL Academic

Post-doc on formal verification and algorithm discovery for numerical analysis

On-site Lausanne, Switzerland

Postdoc
- Lean
- numerical analysis
- AI for mathematics
Checked 2026-10-27

Pay, eligibility and notes
Notes
Chair of Numerical Modelling and Simulation (Annalisa Buffa). Possible projects: formalizing finite-element stability and error estimates in Lean, or AI-assisted discovery of discretizations that are then verified formally. 1-year contract, renewable.
EPFL Academic

Postdoc: Keystone Project (Machine-Verified LLM Inference)

On-site Lausanne, Switzerland (regular visits to Imperial College London)

Postdoc
- Rocq
- Lean
- Isabelle
- HOL
- PTX
- Triton
- ML inference
- GPU kernels
- AI-assisted proof engineering
Checked 2026-10-27

Pay, eligibility and notes
Notes
ARIA-funded EPFL/Imperial project to build a formally verified LLM inference engine (contact: Nate Foster). 1-year renewable contract, start 2026-12-01 or later. The EPFL page states no deadline; one third-party aggregator listed 3 Nov 2026, so treat it as urgent.
EPFL Academic

Postdoc: Networked Systems Abstractions Lab (LASeR)

On-site Lausanne, Switzerland

Postdoc
- NetKAT
- symbolic automata
- decision procedures
- theorem proving
- networking
Checked 2026-10-27

Pay, eligibility and notes
Notes
Nate Foster's lab: languages and formal reasoning tools for networks (NetKAT, routing algebras, packet scheduling). 1-year renewable, start 2026-12-01. No deadline stated.
EPFL Academic

Software Engineer: Keystone Project (Machine-Verified LLM Inference)

On-site Lausanne, Switzerland (regular visits to Imperial College London)

Research engineer
- Rocq
- Lean
- HOL
- Isabelle
- CUDA
- Triton
- ML inference
- GPU kernels
- AI-assisted proof engineering
Checked 2026-10-27

Pay, eligibility and notes
Notes
Engineering role on the same ARIA-funded verified-inference project. Prior formal verification experience is welcome but not required. 1-year renewable, start 2026-12-01. No deadline stated.
Etched Hardware

Formal Verification - DV

On-site San Jose, CA

Senior
- SystemVerilog
- SVA
- hardware
- AI accelerators
Posted 2026-06-10
Checked 2026-10-27

Pay, eligibility and notes
Notes
Covers the full ASIC (compute arrays, NoC, PCIe, Ethernet). Includes a housing subsidy for living near the office.
Galois Software

Principal Scientist

Hybrid Portland, OR / Arlington, VA / Dayton, OH / Minneapolis, MN / Boston, MA

Principal
- formal verification
- theorem proving
- static analysis
- high-assurance software
- defense
- cryptography
- AI
Posted 2026-04-13
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Must be eligible for a US security clearance (active clearance strongly preferred) and must not require an export licence
Notes
Leads externally funded research programs; PhD or equivalent with a publication record in FV.
Galois Software

Research Engineer

Hybrid Portland, OR / Arlington, VA / Dayton, OH / Minneapolis, MN / Boston, MA

Research engineer
- theorem provers
- model checkers
- Haskell
- formal semantics
- high-assurance software
- defense
- cryptography
Posted 2026-01-05
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
US citizenship required (security clearance eligibility)
Notes
Employee-owned; pay is set by a company-wide transparent process rather than published per posting.
General Diffusion Software

Member of Technical Staff, Safety & Formal Verification

On-site San Francisco, CA

Engineer
- model checking
- SMT
- theorem proving
- abstract interpretation
- runtime verification
- AI infrastructure
- compilers
- AI safety
Checked 2026-10-27

Pay, eligibility and notes
Notes
Compute-world-model startup. Owns an independent assurance layer that gates AI-proposed compute actions: machine-checkable safety invariants, refinement/semantic-equivalence validation of generated kernels, runtime monitors. Apply by email (careers@generaldiffusion.com).
Google Hardware

ASIC Formal Verification Engineer, Google Cloud

On-site Sunnyvale, CA

Engineer
- SystemVerilog
- SVA
- Jasper
- VC Formal
- Questa Formal
- 360-DV
- hardware
- AI accelerators
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 138,000–197,000 base + 15% bonus target + equity
Google Hardware

ASIC Formal Verification Engineer, TPU Compute

On-site Sunnyvale, CA

Senior
- SystemVerilog
- SVA
- Jasper
- VC Formal
- Questa Formal
- hardware
- AI accelerators
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 163,000–237,000 base + 15% bonus target + equity
Notes
The work includes formally proving floating-point adders and multipliers. Requires 8 years of experience, although Google labels the level "Mid".
Google Hardware

Senior SoC Formal Verification Engineer, Google Cloud

On-site Tel Aviv / Haifa, Israel

Senior
- SystemVerilog
- SVA
- PSL
- JasperGold
- VC Formal
- Questa Formal
- 360-DV
- hardware
- cloud
Checked 2026-10-27

Pay, eligibility and notes
Notes
Google's Israel team for custom server chips.
Google DeepMind AI for proof & autoformalization

Lean Theorem Proving Engineer, Verified Code Generation, DeepMind

On-site London, UK / Mountain View, CA

Engineer
- Lean
- AI for code
- program verification
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 174,000–252,000 plus 15% bonus target and equity (US)
Notes
Successor to the archived Research Scientist, Verified Code Generation role. Requires a PhD or equivalent, 3 years with Lean and 3 years using AI agents. The work formalizes C/C++/Rust semantics and correctness specs in Lean with AI help, and builds infrastructure for proof search at scale.
Harmonic AI for proof & autoformalization

Formal Verification Engineer (Aristotle)

On-site Palo Alto, CA / London, UK

Engineer
- Lean
- AI for mathematics
- hardware
- software verification
Posted 2026-08-13
Checked 2026-10-27

Pay, eligibility and notes
Notes
Customer-facing; scope properties, run proofs with Aristotle, diagnose failures.
Harmonic AI for proof & autoformalization

Research Engineer

On-site Palo Alto, CA

Research engineer
- Lean
- theorem proving
- reinforcement learning
- AI for mathematics
- theorem proving
Posted 2025-07-10
Checked 2026-10-27

Pay, eligibility and notes
Notes
Reinforcement Learning & Formal Methods team: new RL algorithms and models for mathematical theorem proving behind Aristotle (Lean 4). Separate from the two Harmonic roles already on the board.
Harmonic AI for proof & autoformalization

Research Engineer, Formal Methods

On-site Palo Alto, CA / London, UK

Research engineer
- Lean
- Rocq
- Isabelle
- Agda
- Python
- AI for mathematics
- theorem proving
Posted 2026-08-24
Checked 2026-10-27
IBM Hardware

Formal Verification Engineer

Hybrid Bangalore, India

Senior
- SVA
- Verilog
- VHDL
- Python
- hardware
- CPU
Posted 2026-10-13
Checked 2026-10-27

Pay, eligibility and notes
Notes
The posting body calls the role "Formal Verification Lead". The work covers IBM server-class processors, SoCs and ASICs, using IBM internal formal tools.
Inria (Argo team, Paris) Academic

Advanced Research Position: AI for formal mathematics (quality, evaluation and translation of LLM-generated proofs)

On-site Paris, France

Research scientist
- Lean
- Mathlib
- Rocq
- Mathematical Components
- AI for mathematics
- formalized mathematics
Checked 2026-10-27

Pay, eligibility and notes
Notes
BELLE project (AI for Math Fund). Leads the LLM axis: quality metrics for AI-generated Lean code, the BELLE-Prefs dataset and GRPO fine-tuning, and supervises a postdoc. 12-month renewable contract, start 2026-12-01. Ad in French. Deadline 2026-11-14.
Inria (Rennes) Academic

PhD Position: Trustable Machine Learning: Analysis and Verification of Soft Automata

On-site Rennes, France

PhD
- neural network verification
- automata learning
- trustworthy ML
Checked 2026-10-27

Pay, eligibility and notes
Pay
EUR 2,300 gross/month
Notes
Part of the SAIF ("Safe AI through Formal methods") project. 3-year contract. Deadline 2026-11-07.
Intel Hardware

Formal Verification Engineer

On-site Haifa / Jerusalem / Petah Tikva, Israel

Engineer
- Jasper
- SVA
- model checking
- equivalence checking
- hardware
- networking
Posted 2026-10-06
Checked 2026-10-27

Pay, eligibility and notes
Notes
Intel Networking (Ethernet) team.
Intel Hardware

Senior Formal Verification Engineer – AI SoC Development

Hybrid Folsom, CA / Santa Clara, CA / Hillsboro, OR / Austin, TX

Senior
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- Questa Formal
- hardware
- AI accelerators
Posted 2026-02-20
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 220,920–311,890
Work authorization
Position of Trust: extended background investigation required
Jane Street Software

Formal Methods Engineer

On-site London, UK (also New York)

Engineer
- proof assistants
- static analysis
- refinement types
- property-based testing
- finance
- AI-assisted programming
Checked 2026-10-27

Pay, eligibility and notes
Notes
New team; no OCaml or functional programming experience required.
Johns Hopkins Applied Physics Laboratory Software

2027 PhD Graduate - Formal Verification and Software Assurance Engineer

On-site Laurel, MD

Engineer
- model checking
- interactive theorem proving
- automated theorem proving
- abstract interpretation
- symbolic execution
- defense
- cybersecurity
- cyber-physical systems
Posted 2026-09-01
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 105,000–245,000
Work authorization
U.S. citizenship required; must obtain Interim Top Secret clearance by start date
Notes
For PhD graduates (2027 start). Rolling applications.
LUBIS EDA Hardware

Formal Verification Engineer - Professional Level

Hybrid Kaiserslautern, Germany

Engineer
- SVA
- Jasper
- VC Formal
- Questa Formal
- OneSpin
- hardware
- EDA services
Posted 2026-03-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Formal verification consultancy for clients' RTL.
LUBIS EDA Hardware

Formal Verification Engineer - Senior Level

Hybrid Kaiserslautern, Germany

Senior
- SVA
- hardware
- EDA services
Posted 2026-05-20
Checked 2026-10-27
LUBIS EDA Hardware

Manager Formal Verification (m/f/d)

Hybrid Kaiserslautern, Germany

Lead
- SVA
- hardware
- EDA services
Posted 2026-09-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Leads a team of 10–15 formal verification engineers. This is a people and customer management role.
Marvell Hardware

Senior Engineer, Logic Equivalence CAD

On-site Bangalore, India

Senior
- logical equivalence checking
- hardware
- EDA tools
Posted 2026-10-14
Checked 2026-10-27

Pay, eligibility and notes
Notes
CAD role owning company-wide RTL-to-gate and gate-to-gate equivalence checking flows.
Math, Inc. AI for proof & autoformalization

Open applications (verified mathematics)

Remote (worldwide) Not stated

Various
- Lean
- AI for mathematics
- autoformalization
Checked 2026-10-27

Pay, eligibility and notes
Notes
Makers of Gauss, an autoformalization agent that works in Lean. The page is a general application form asking for "evidence of extraordinary ability"; internships go through math.inc/careers/intern. Location and remote policy are not stated. Third-party bios place the company in Palo Alto.
Mathlib Initiative AI for proof & autoformalization

Open applications — part-time reviewers and autoformalization expert (Formal Frontier team)

Remote (worldwide) Not stated

Various
- Lean
- mathlib
- formal mathematics
- AI for mathematics
Checked 2026-10-27

Pay, eligibility and notes
Notes
A Renaissance Philanthropy program. Takes applications for part-time contract reviewers and a part-time autoformalization expert on the Formal Frontier team. Successful applicants usually already contribute to major formal-math libraries. The published contact is info@mathlib-initiative.org.
MatX Hardware

Formal Verification Engineer

Remote Mountain View, CA (HQ) or Remote

Various
- JasperGold
- VC Formal
- SymbiYosys
- SVA
- Lean
- Rocq
- Isabelle
- hardware
- AI accelerators
- compilers
Posted 2026-05-19
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 160k–275k (early career), 175k–400k (mid), 250k–600k (senior), plus equity
Work authorization
US export control: must be able to work without an export licence
Notes
Combines RTL model checking with HDL embeddings in interactive theorem provers and machine-checked compiler-lowering proofs.
Mercor AI for proof & autoformalization

Lean Engineer, Formal Mathematics (Lean 4, Mathlib, Theorem Proving)

Remote (worldwide) Remote

Engineer
- Lean
- mathlib
- AI for mathematics
- AI training data
Posted 2026-09-30
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 90–110/hour, part-time (20–40 hours/week)
Work authorization
Mercor states it cannot support H-1B or STEM OPT candidates
Notes
Placement at an unnamed "leading AI lab". Write and review Lean 4 proofs, formalize informal mathematics, and check whether AI-generated proofs prove the right statement. The posting calls it both W-2 employment through Cincinnatus LLC (or an international entity) and independent contracting.
Microsoft Software

Post Doc Researcher (FoSSE, Microsoft Research India)

On-site Bangalore, India

Postdoc
- formal methods
- static analysis
- programming languages
- software engineering
- code migration
Posted 2026-08-20
Checked 2026-10-27

Pay, eligibility and notes
Notes
Req 200049580. FoSSE team works on code migration, translation and static analysis "using AI and formal methods".
Microsoft Hardware

Principal Design Verification Engineer - Formal

On-site Raleigh, NC / Austin, TX / Hillsboro, OR / Mountain View, CA

Principal
- SystemVerilog
- SVA
- hardware
- cloud
- interconnect
Posted 2026-10-23
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 142,800–274,800 base (US typical); USD 188,000–304,200 (SF Bay Area / NYC)
Work authorization
Export-controlled (ITAR/EAR) access: proof of citizenship or US residency/protected status required; Microsoft Cloud Background Check
Notes
SCHIE / Compute Silicon (Azure Cobalt); formal verification of fabric interconnect IP.
Microsoft Hardware

Principal Formal Design Verification Engineer

On-site Bangalore, India

Principal
- SystemVerilog
- SVA
- hardware
- cloud
- interconnect
Posted 2026-10-15
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Export-controlled information: proof of citizenship/residency for eligibility assessment; Microsoft Cloud Background Check
Microsoft Software

Principal Researcher and Senior Principal Researcher - Software Verification - Microsoft Research

On-site Redmond, WA

Principal
- formal methods
- systems software verification
- AI agents
- systems software
- AI for verification
Posted 2026-10-14
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 142,800–274,800 (Principal) / 165,600–296,400 (Senior Principal); higher bands in SF Bay Area and NYC
Notes
Req 200061832. Research on AI and agents for "rapid development of vast amounts of verified systems code".
Microsoft Software

Principal Software Engineer (AI-driven code transformation with formal verification)

On-site Bangalore, India

Principal
- Verus
- F*
- Lean
- TLA+
- Dafny
- CodeQL
- developer tools
- code migration
Posted 2026-10-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Req 200063311 (posting title is just "Principal Software Engineer"). Agentic code migration backed by Verus proofs and spec inference. A Senior Software Engineer twin is req 200063310 (job/1970393557045291).
Microsoft Software

Senior Researcher - Software Verification - Microsoft Research

On-site Redmond, WA

Research scientist
- SMT
- automated reasoning
- program verification
- systems software
- AI for verification
Posted 2026-10-14
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 119,800–234,700 (US); USD 160,200–261,000 (SF Bay Area, NYC)
Notes
Req 200061829. Develops automated reasoning tools including SMT solvers (the Z3 / RiSE lineage, though the posting does not name Z3).
Microsoft Software

Senior Software Engineer (AI-driven code transformation with formal verification)

On-site Bangalore, India

Senior
- Verus
- F*
- Lean
- TLA+
- Dafny
- CodeQL
- developer tools
- code migration
Posted 2026-10-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Req 200063310 (posting title is just "Senior Software Engineer"). Same team as req 200063311.
Mistral AI AI for proof & autoformalization

Applied Scientist - Research Engineer (Formal Methods), EMEA

On-site Paris, France / London, UK

Research engineer
- Lean
- proof assistants
- autoformalization
- AI for mathematics
- software verification
Posted 2026-10-20
Checked 2026-10-27

Pay, eligibility and notes
Notes
Train and post-train LLMs for formal reasoning. Build theorem-proving and software-verification datasets, evaluators and benchmarks. RL from Lean verifiable rewards is a plus. The posting does not state a workplace type.
Mobileye Hardware

Experienced Formal Verification Engineer

On-site Haifa, Israel

Senior
- JasperGold
- SystemVerilog
- hardware
- automotive
- autonomous driving
Checked 2026-10-27

Pay, eligibility and notes
Notes
Automated Driving Hardware group; 5+ years of formal verification experience required.
National University of Singapore Academic

Postdoctoral and PhD positions — Foundations for Testing and Verifying Concurrency in Go (Umang Mathur)

On-site Singapore

Postdoc
- mechanized semantics
- model checking
- predictive analysis
- concurrency
- compilers
Posted 2026-09-15
Checked 2026-10-27

Pay, eligibility and notes
Notes
Also recruiting PhD students. The FOCS Lab project includes mechanized Go concurrency semantics with compiler-correctness proofs. Enquire by email; no deadline.
Nuvacore Hardware

Formal Verification Engineer

Hybrid Austin, TX (also Santa Clara, CA; Markham, ON; Bangalore)

Senior
- JasperGold
- VC Formal
- Questa Formal
- SystemVerilog Assertions
- model checking
- equivalence checking
- hardware
- CPUs
Posted 2026-09-18
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 140,000–250,000
Notes
CPU startup; Senior (4+ yrs) to Principal (15+ yrs); cache coherence, memory consistency, speculation. Theorem proving listed as a plus.
NVIDIA AI for proof & autoformalization

AI Compiler Formal Verification Intern

On-site Zurich, Switzerland

Intern
- Lean
- SMT
- compilers
- AI infrastructure
Posted 2026-10-20
Checked 2026-10-27

Pay, eligibility and notes
Notes
Research and implement formal methods to verify AI compiler passes, IRs and lowerings, using AI and semantic verification. A strong formal-methods background (preferably a PhD) is expected.
NVIDIA AI for proof & autoformalization

Engineering Manager, AI Compiler Analysis

On-site Santa Clara, CA / Austin, TX / Seattle, WA

Lead
- Lean
- SMT
- theorem proving
- fuzzing
- compilers
- AI infrastructure
Posted 2026-10-16
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 168,000–270,250 (Level 2); USD 200,000–322,000 (Level 3)
Notes
Leads AI-compiler quality work. Includes setting formal-verification requirements for compiler transformations and generated GPU programs, alongside fuzzing and differential testing.
NVIDIA Hardware

Formal Verification Engineer - New College Grad 2026

On-site Santa Clara, CA

Engineer
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- hardware
- GPU
- CPU
Posted 2026-10-06
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 100,000–166,750 (L1) / 116,000–189,750 (L2) base + equity
NVIDIA Software

Senior Compute System Software Engineer

On-site Bengaluru, India

Senior
- Lean 4
- TLA+
- Haskell
- GPU drivers
- safety-critical software
Posted 2026-09-21
Checked 2026-10-27

Pay, eligibility and notes
Notes
Bootstraps formal verification of the software architecture and design of Tegra user-mode compute drivers, and defines a company-wide formal verification process.
NVIDIA Hardware

Senior Formal Verification Engineer

On-site Santa Clara, CA / Austin, TX

Senior
- SystemVerilog
- SVA
- hardware
- GPU
Posted 2026-09-23
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 136,000–218,500 (L3) / 168,000–264,500 (L4) base + equity
NVIDIA Hardware

Senior Formal Verification Engineer - LPU

Remote US remote (CA, TX, CO, OR, WA, MA)

Senior
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- hardware
- AI accelerators
Posted 2026-07-06
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 136,000–218,500 (L3) / 168,000–264,500 (L4) base + equity
Notes
LPU (the Groq-derived inference architecture). Two more LPU formal reqs are open, one remote US and one remote Canada.
NVIDIA Hardware

Senior Research Scientist, AI-Enabled Secure Systems

On-site Westford, MA / Santa Clara, CA

Research scientist
- theorem provers
- formal verification
- program analysis
- synthesis
- security
- AI for code
- hardware
Posted 2026-10-22
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 224,000–356,500 (Level 5); USD 272,000–431,250 (Level 6)
Notes
Combine generative AI and agents with formal methods, program analysis and synthesis to design and verify secure hardware and software, including building and checking proofs.
Oath Technologies Software

Formal Methods Research Engineer

On-site Berkeley, CA

Research engineer
- Lean
- Coq
- Isabelle
- SMT
- AI safety
- AI oversight
Posted 2026-09-09
Checked 2026-10-27

Pay, eligibility and notes
Notes
Formal methods tooling for AI oversight, starting with verified agent containment. Wants direct proof-assistant or SMT experience, plus PL theory or a record of moving formal methods into deployed systems. Hiring runs through Convergent Research's board.
Oath Technologies Software

Research Engineer, Tools & Infrastructure

On-site Berkeley, CA

Research engineer
- developer tooling
- language servers
- agent scaffolding
- AI safety
- developer tools
Posted 2026-09-09
Checked 2026-10-27

Pay, eligibility and notes
Notes
IDE integrations, language servers, CLI and build-system work for formal methods tools. Prior formal methods depth is explicitly not required.
Pramaana Labs AI for proof & autoformalization

Research Engineer

On-site Palo Alto, CA (also Bengaluru, India)

Research engineer
- Lean
- Coq
- Isabelle
- SMT
- AI for formal reasoning
- law
- tax
Posted 2026-10-26
Checked 2026-10-27

Pay, eligibility and notes
Notes
Builds and improves the domain formalizer, autoformalizer and prover with the formal-methods engineers. The posting says prior formal verification experience is not required.
Pramaana Labs AI for proof & autoformalization

Research Intern

On-site Palo Alto, CA (also Bengaluru, India)

Intern
- Lean
- Coq
- Isabelle
- AI for formal reasoning
Posted 2026-09-23
Checked 2026-10-27

Pay, eligibility and notes
Notes
Possible areas: model training, harness engineering, AI-for-formal research and benchmarks. Includes designing harnesses for autoformalization and prover systems.
Pramaana Labs AI for proof & autoformalization

Research Scientist, AI

On-site Palo Alto, CA (also Bengaluru, India)

Research scientist
- Lean
- AI for formal reasoning
- law
- tax
Posted 2026-10-26
Checked 2026-10-27

Pay, eligibility and notes
Notes
Improves the accuracy, coverage and generalization of the domain formalizer, autoformalizer and prover. Works with formal-methods experts on whether model outputs are faithful to the source.
Pramaana Labs AI for proof & autoformalization

Research Scientist, Reinforcement Learning

On-site Palo Alto, CA

Research scientist
- Lean
- AI for formal reasoning
- law
- tax
- healthcare
Posted 2026-08-24
Checked 2026-10-27

Pay, eligibility and notes
Notes
Pramaana (founded 2025; $27M seed led by Khosla, June 2026) formalizes tax codes, legal rules and clinical guidelines into a Lean 4 "symbolic world model". This role scales RLVR with the Lean kernel as reward and pushes autoformalization and proof search.
Qualcomm Hardware

CPU Formal Verification Engineer

On-site Santa Clara, CA

Senior
- JasperGold
- VC Formal
- ACL2
- HOL
- hardware
- CPU
Posted 2026-09-17
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 147,900–221,900
Notes
End-to-end formalisation of the refinement from architecture to microarchitecture. Domain knowledge wanted in ISA, floating point, memory consistency and coherency.
Qualcomm Hardware

Formal Verification Senior Engineer - Qualcomm, Cambridge, UK

On-site Cambridge, United Kingdom

Engineer
- SystemVerilog
- SVA
- JasperGold
- VC Formal
- hardware
- GPU
Posted 2026-09-04
Checked 2026-10-27

Pay, eligibility and notes
Notes
Requires 2+ years of FV experience. DPV and C2RTL/RTL2RTL sequential equivalence experience is a plus.
Qualcomm Hardware

Senior Staff Formal Verification Engineer

On-site San Diego, CA / Austin, TX / Santa Clara, CA

Senior
- SystemVerilog
- SVA
- hardware
- GPU
Posted 2026-09-17
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 203,700–305,500
Notes
Adreno GPU.
Quantinuum Software

Advanced Quantum Compiler Engineer (925)

Hybrid Broomfield, CO

Engineer
- LLVM
- MLIR
- QIR
- Rust
- C++
- quantum
- compilers
Posted 2026-08-03
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 138,000–173,000
Work authorization
US Person required (citizen, green card, refugee or asylee)
Resolution AI for proof & autoformalization

Lean Engineer

Hybrid Berkeley, CA

Engineer
- Lean
- mathlib
- autoformalization
- AI safety
- alignment theory
- formal mathematics
Posted 2026-10-06
Checked 2026-10-27

Pay, eligibility and notes
Pay
Research Engineer levels L4–L7: USD 346,000–930,000 in person, USD 208,000–558,000 remote
Work authorization
Visa sponsorship offered for relocation to Berkeley
Notes
ASI-alignment lab founded in 2026 by former UK AISI alignment staff and Timaeus. The first dedicated Lean hire: sets conventions, shared libraries and review harnesses so agent-written autoformalizations can be trusted at scale. The posting says the job is mostly not writing Lean by hand. Based in Berkeley; remote only in exceptional cases.
RTX BBN Technologies Software

Research Software Engineer, Formal Methods (Hybrid) — Networking and Cyber Technologies

Hybrid Cambridge, MA / Arlington, VA / Columbia, MD

Research engineer
- model checking
- theorem proving
- SAT
- SMT
- defense
- network security
- protocols
Posted 2026-04-01
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 86,800–165,200
Work authorization
US citizenship required (must be able to obtain a security clearance)
Notes
Same title as req 01878215 but a different BBN group, and no existing clearance required.
RTX BBN Technologies Software

Research Software Engineer, Formal Methods (Hybrid) — Non-Kinetic Capabilities and Technologies

On-site Cambridge, MA / Arlington, VA / Columbia, MD

Research engineer
- model checking
- theorem proving
- SAT
- SMT
- defense
- network security
- protocols
Posted 2026-09-29
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 86,800–165,200
Work authorization
US citizenship required; active Top Secret clearance required
Notes
The title says Hybrid but the posting body lists the role type as onsite.
Runtime Verification Cryptocurrency

Open applications — verification engineering (K framework)

Remote Urbana, IL — remote friendly

Various
- K framework
- executable semantics
- blockchain
- language semantics
Checked 2026-10-27
RWTH Aachen University (Chair for Quantum Information Systems) Academic

PhD positions — Certified quantum compilation; Verification of quantum cryptography; Type systems for quantum programming languages (postdocs also welcome)

On-site Aachen, Germany

PhD
- machine-checked proofs
- type systems
- quantum computing
- cryptography
- compilers
Checked 2026-10-27

Pay, eligibility and notes
Pay
TV-L E13
Notes
Dominique Unruh's group. The soft deadline (end of September 2026) has passed; the pages say later applications are considered only if the position is still unfilled.
Samsung Semiconductor (SARC/ACL) Hardware

Senior Staff Engineer, GPU Design Verification (Formal Verification)

On-site San Jose, CA

Senior
- SystemVerilog
- SVA
- hardware
- GPU
Posted 2026-10-08
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 198,200–297,200 base
Work authorization
May require access to US export-controlled information; must be authorized or eligible for government authorization
Samsung Semiconductor (SARC/ACL) Hardware

Staff GPU Design Verification Engineer – Formal Verification

On-site Austin, TX

Senior
- SystemVerilog
- SVA
- hardware
- GPU
Posted 2026-10-12
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 151,000–226,600 base
Work authorization
May require access to US export-controlled information; must be authorized or eligible for government authorization
Notes
Xclipse mobile GPU; clock/power-gating formal.
Sandia National Laboratories Software

Intern, R&D Graduate Year Round - Formal Verification

On-site Livermore, CA

Intern
- Rocq
- CompCert
- VST
- Flocq
- separation logic
- Isabelle/HOL
- compilers
- firmware
- hardware
- numerical software
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
US citizens, permanent residents, asylees or refugees; nationals of China, Iran, North Korea or Russia barred unless also US citizens; no clearance required
Notes
Req 699392. Enrolled full-time graduate students; up to 30 hours/week during term.
SF Tensor Software

Member of Mathematical Staff

On-site San Francisco, CA

Research scientist
- Lean
- Rocq
- SMT
- Mathlib
- Flocq
- compilers
- GPU kernels
- AI for mathematics
Posted 2026-09-27
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 225,000–315,000 base plus equity
Notes
YC-backed GPU compiler that proves kernel correctness after search; role owns the proof engine, formal models of new hardware and floating-point / low-precision formalisation. PhD in maths strongly recommended but not required.
SiFive Hardware

Distinguished Formal Verification Architect

On-site Santa Clara, CA / Austin, TX / Boston, MA

Principal
- VC Formal
- JasperGold
- SAT
- SMT
- theorem proving
- hardware
- CPU
- RISC-V
Posted 2026-09-21
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 279,504–341,616 base
Work authorization
Offer contingent on authorization for access to export-controlled technology (or obtaining a licence)
Notes
Functional programming (Scala/OCaml/Haskell) and theorem-prover familiarity are nice-to-haves.
SiFive Hardware

Senior CPU Formal Verification Engineer

On-site Hyderabad / Bengaluru, India

Senior
- SystemVerilog
- SVA
- hardware
- CPU
- RISC-V
Posted 2026-10-26
Checked 2026-10-27
SiFive Hardware

Staff Design Verification Engineer – CPU Core Formal Verification

On-site Austin, TX / Santa Clara, CA

Senior
- SystemVerilog
- SVA
- hardware
- CPU
- RISC-V
Posted 2026-09-13
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Offer contingent on authorization for access to export-controlled technology (or obtaining a licence)
Notes
Formal work on out-of-order RISC-V core units such as the frontend, issue/commit and the load-store unit. Three identical reqs are open (R-101462, R-101463, R-101466).
Snowflake Software

Principal / Staff Applied Research Scientist

On-site Menlo Park, CA

Principal
- model checking
- theorem proving
- SAT/SMT
- program verification
- program analysis
- databases
- distributed systems
- cloud
Posted 2026-09-02
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 236,000–339,200
Notes
New applied-research line on "verified data infrastructure": formal methods and automated reasoning applied to Snowflake's distributed systems and developer tooling. Hiring at Staff or Principal level; PhD (or equivalent) and 8+ years expected. Workplace arrangement not stated.
Sorbonne Paris North University (LIPN) Academic

PhD Position in Strategy Logics (verification and synthesis for multi-agent systems)

On-site Villetaneuse (Paris area), France

PhD
- model checking
- ATL
- synthesis
- multi-agent systems
Checked 2026-10-27

Pay, eligibility and notes
Notes
Supervisor Munyque Mittelmann. Apply by email. Deadline 2026-11-15.
Synopsys Hardware

Principal Application Engineer, VC Formal

On-site Bengaluru, India

Principal
- VC Formal
- SVA
- EDA tools
- hardware
Posted 2026-09-20
Checked 2026-10-27
Synopsys Hardware

Senior Staff Formal Verification Applications Engineer

On-site Sunnyvale, CA

Senior
- VC Formal
- SVA
- EDA tools
- hardware
Posted 2026-09-27
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 157,000–235,000 base
Notes
Customer-facing VC Formal deployment role covering property checking, DPV, SEQ and connectivity.
Tenstorrent Hardware

Formal Verification Engineer

Remote North America or Spain (listed Santa Clara, CA; Spain)

Senior
- SystemVerilog
- SVA
- hardware
- CPU
- RISC-V
- AI accelerators
Posted 2026-10-05
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 100k–500k company-wide engineer range (base + variable); role-specific band not given
Work authorization
US export control (EAR): offer may be contingent on citizenship/permanent residency or a licence
Notes
Posting says candidates at various experience levels are welcome; 6+ years listed.
Thales Software

Stage en IA : automatisation de la conformité d'un référentiel documentaire et génération d'un code sécurisé

On-site Gennevilliers, France

Intern
- Coq
- OCaml
- security
- verified software
Posted 2026-10-26
Checked 2026-10-27

Pay, eligibility and notes
Notes
Master's-level (Bac+4/5) internship. Despite the AI title, the task is a data filter developed and proved correct in Coq, then extracted to OCaml.
Thales Software

STAGE – Ingénieur Automatisation agentique d'analyse statique de code C – F/H

On-site Toulouse, France

Intern
- Frama-C
- C
- embedded security
- static analysis
Posted 2026-10-21
Checked 2026-10-27

Pay, eligibility and notes
Notes
Six-month engineering internship building an MCP server that exposes Frama-C to an AI agent.
Theorem (Theorem Labs) AI for proof & autoformalization

Systems Engineer / ML Researcher / research fellowship

On-site San Francisco, CA

Various
- Lean
- Rocq
- AI for program verification
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 200,000–500,000 plus equity; fellowship USD 125,000/yr pro rata
Notes
Built lf-lean, an AI-assisted verified Rocq-to-Lean translation.
Trail of Bits Software

Senior Security Engineer, Research & Engineering (United Kingdom)

Remote United Kingdom

Senior
- Lean
- Rocq
- F*
- Dafny
- Verus
- security assurance
- verified systems
Posted 2026-09-02
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Remote within the United Kingdom
Notes
Attacks formally verified systems by mapping what a proof does and does not establish, then demonstrating gaps with working exploits.
TrustInSoft Software

AI Engineer

On-site Paris, France

Engineer
- formal methods
- C
- OCaml
- static analysis
- AI for verification
Checked 2026-10-27

Pay, eligibility and notes
Notes
Joins the 15-person R&D team behind TrustInSoft Analyzer (a Frama-C derivative); OCaml can be learned on the job. The posting promises a "flexible working environment" but states no remote policy.
TU Braunschweig Academic

PhD Positions in Formal Methods for Trustworthy Systems and AI

On-site Braunschweig, Germany

PhD
- model checking
- automated reasoning
- Rust
- AI
- explainability
Checked 2026-10-27

Pay, eligibility and notes
Pay
TV-L E13
Notes
New group led by Clemens Dubslaff, several full-time PhD positions. Apply by email. Deadline 2026-12-07 (per ILLC listing).
TU Delft Academic

PhD Position: Systematic Derivation of Formal Languages and Their Correctness

On-site Delft, Netherlands

PhD
- Agda
- Rocq
- Lean
- type theory
- programming languages
Checked 2026-10-27

Pay, eligibility and notes
Pay
EUR 3,204–4,051 gross/month (years 1–4)
Notes
AFOSR-funded SemSyn project (Benedikt Ahrens): dependent type theory, two-level type theory, with formalization in Agda. 4 years (1.5 + 2.5). Rolling review. Deadline 2026-11-29.
University of East Anglia Academic

PhD Studentship: Formalising the Local Langlands Correspondence for GL₂(F) in Lean

On-site Norwich, UK

PhD
- Lean
- formalized mathematics
- number theory
Checked 2026-10-27

Pay, eligibility and notes
Notes
Self-funded: no stipend, and a bench fee is payable. Supervisor Christopher Birkbeck. Start 2027-02-01. Deadline 2026-11-30.
University of Edinburgh (Quantum Software Lab) Academic

Research Associate — RubberDUQ project (semantics and correct-by-construction compilation for hybrid quantum-classical programs)

Hybrid Edinburgh, UK

Postdoc
- categorical semantics
- compiler correctness
- quantum computing
- compilers
Posted 2026-10-21
Checked 2026-10-27

Pay, eligibility and notes
Pay
GBP 41,064–48,822
Notes
12-month fixed-term, to 31/12/2027. Job ref 15102. Deadline 2026-11-04.
University of Exeter Academic

PhD in End-to-End Verification of Security Protocols in Isabelle

On-site Exeter, UK

PhD
- Isabelle/HOL
- zero-knowledge proofs
- cryptography
- compilers
- security protocols
Posted 2026-10-27
Checked 2026-10-27

Pay, eligibility and notes
Pay
UK tuition fees plus GBP 21,805/year stipend (3.5 years)
Work authorization
EPSRC Doctoral Landscape Award residence criteria apply. The jobs.ac.uk advert lists funding for UK, EU and international students.
Notes
One of several projects competing in the EPSRC DLA studentship round for September 2027 entry. Deadline 2026-12-08 (midday).
University of Strathclyde (Mathematically Structured Programming group) Academic

PhD scholarships 2027 (John Anderson Research Studentship Scheme)

On-site Glasgow, UK

PhD
- dependent types
- proof automation
- model checking
- type theory
- programming languages
Posted 2026-10-26
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
Funding covers UK Home fees only ("not enough for non-UK tuition fees").
Notes
Competitive scheme with several fully funded places. Contact a potential supervisor before 2026-12-01; candidacy decision 2026-12-11.
Uppsala University Academic

PhD student — Scalable Verification of Quantum Programs

On-site Uppsala, Sweden

PhD
- program verification
- automated theorem proving
- quantum computing
Posted 2026-08-21
Checked 2026-10-27

Pay, eligibility and notes
Work authorization
The position may be subject to security vetting ("Anställningen kan komma att säkerhetsprövas").
Notes
Department of Information Technology. Ad in Swedish. Start 2027-01-15. Deadline 2026-11-15.
Velaura Hardware

Senior Formal Verification Engineer

On-site Santa Clara, CA / Bangalore, India

Senior
- SystemVerilog Assertions
- JasperGold
- VC Formal
- Questa Formal
- OneSpin
- bounded model checking
- equivalence checking
- hardware
- robotics
- physical AI
Posted 2026-07-25
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 200,000–300,000 base plus equity
Notes
Physical-AI SoC startup; formal for CPUs, FPUs (IEEE-754), vector/SIMD; 10+ years expected.
Veridise Cryptocurrency

Formal Methods Researcher for ZK

Remote Flexible

Research scientist
- Lean
- Rocq
- ACL2
- SMT
- Rust
- C++
- zero-knowledge
- blockchain security
Posted 2026-01-21
Checked 2026-10-27

Pay, eligibility and notes
Notes
PhD or equivalent professional research experience requested.
Waymo Hardware

Senior Formal Verification Engineer

Hybrid Mountain View, CA

Senior
- JasperGold
- VC Formal
- Questa Formal
- SystemVerilog Assertions
- bounded model checking
- sequential equivalence checking
- hardware
- automotive
- autonomous vehicles
Posted 2026-02-09
Checked 2026-10-27

Pay, eligibility and notes
Pay
USD 204,000–259,000 base
Notes
Owns formal sign-off for Waymo's custom autonomous-driving silicon.
YosysHQ Hardware

Synthesis or Formal Verification Developer at YosysHQ

Remote (worldwide) Anywhere

Engineer
- Yosys
- SymbiYosys
- SAT
- SMT
- C++
- Rust
- Python
- EDA tools
- open source
Posted 2025-09-01
Checked 2026-10-27

Pay, eligibility and notes
Pay
EUR 6,000/month full-time (flat rate for everyone); part-time possible
Work authorization
Freelance contract with an Austrian company; candidates must not live in a sanctioned/export-restricted country or be barred from US-government work
Notes
Maintainers of Yosys and the open-source EDA stack. The posting has a formal track (hardware model checking implementation) and a synthesis track.

Closed roles (3)

Kept because knowing a company hired for Lean work six months ago is useful even when the posting is gone.

Cryspen Software

Open applications (Rust verification, hax)

Hybrid France / Germany

Various
- hax
- Rust
- F*
- cryptography
Closed 2026-10-27

Pay, eligibility and notes
Notes
No individual postings listed; speculative applications via info@cryspen.com.
Google DeepMind AI for proof & autoformalization

Research Scientist, Verified Code Generation

On-site Mountain View, CA / London, UK

Research scientist
- Lean
- AI for code
- program verification
Closed 2026-10-26

Pay, eligibility and notes
Pay
USD 174,000–252,000 plus 15% bonus and equity
Notes
Formalizing C/C++ semantics in Lean, verified static analyses, and AI-driven proof search. Both posting IDs returned "job not found" on 2026-10-26.
Imandra Software

Open applications — R&D (automated reasoning)

Remote Edinburgh / London / Bristol / Austin

Various
- OCaml
- SMT
- automated reasoning
- finance
- automated reasoning
Closed 2026-10-27

Jobs in formal verification

Open roles