FVjobs
Γ ⊢ you : Lean ∨ Rocq ∨ Isabelle ∨ SMT Γ ⊢ live(posting, 2026-11-02)
apply
Γ ⊢ ∃ j ∈ jobs. you fit j

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.

136 open roles at 84 companies. Maintained alongside Type Theory Forall.

FVjobs is maintained by the community, and you are very welcome to help.

  • Submit a new job you have seen posted.
  • Press Report a problem on any card whose posting has closed, moved or changed. One report is enough.
  • Suggest a change to the site: a filter, the layout, anything that would make it more useful.

Each one is a short GitHub form.

  1. &Truth Software

    Open applications (formal verification, Lean)

    On-site Palo Alto, CA / Singapore

    Various

    • Lean
    • theorem proving
    • formal verification
    • programming languages
    • software verification
    • security
    • AI safety

    FV-148
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    A public benefit corporation building technology to prove code in any language safe, secure and correct, with independently checkable proofs. A general application rather than a specific opening: the careers page names formal verification, theorem proving, programming languages and Lean as the foundation, alongside product, forward-deployed and go-to-market roles.
    Report a problem

  2. Access Softek Toolchains Software

    Compiler Developer (LLVM, C++)

    Remote (worldwide) Anywhere

    Engineer

    • LLVM
    • Clang
    • C++
    • compilers
    • toolchains

    FV-001
    Posted
    Checked

    Pay, eligibility and notes
    Work authorization
    No restriction stated; "work from anywhere in the world"
    Report a problem

  3. Advanced Micro Devices (AMD) Hardware

    CPU Formal Verification Engineer

    On-site Cambridge, United Kingdom

    Senior

    • SystemVerilog
    • SVA
    • JasperGold
    • VC Formal
    • hardware
    • CPU

    FV-003
    Posted
    Checked

    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.
    Report a problem

  4. 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

    FV-004
    Posted
    Checked

    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.
    Report a problem

  5. 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

    FV-005
    Posted
    Checked

    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.
    Report a problem

  6. 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

    FV-006
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Six months starting around March 2027, in the Avionics Software department (flight controls and related critical software).
    Report a problem

  7. 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

    FV-007
    Posted
    Checked

    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.
    Report a problem

  8. 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

    FV-008
    Posted
    Checked

    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.
    Report a problem

  9. 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

    FV-009
    Posted
    Checked

    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.
    Report a problem

  10. Amazon (Annapurna Labs) Hardware

    Senior Formal Verification Engineer, Annapurna Labs

    On-site Haifa, Israel

    Lead

    • SystemVerilog
    • SVA
    • hardware
    • CPU
    • cloud

    FV-010
    Posted
    Checked

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

  11. 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

    FV-011
    Posted
    Checked

    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.
    Report a problem

  12. 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

    FV-012
    Posted
    Checked

    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.
    Report a problem

  13. Amazon Web Services Software

    Applied Scientist, Automated Reasoning

    On-site Multiple US cities

    Research scientist

    • Lean
    • Rocq
    • Dafny
    • Isabelle
    • SMT
    • cloud
    • cryptography
    • AI safety

    FV-013
    Posted
    Checked

    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.
    Report a problem

  14. Amazon Web Services Software

    Principal Applied Scientist, Neuro-Symbolic AI Labs

    On-site Boston, MA

    Principal

    • proof assistants
    • AI for reasoning
    • AI for mathematics

    FV-014
    Posted
    Checked

    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.
    Report a problem

  15. Amazon Web Services Software

    Sr Applied Scientist, Amazon Cryptographic Libraries

    On-site Seattle, WA

    Senior

    • HOL Light
    • Verus
    • CBMC
    • Lean
    • cryptography
    • post-quantum cryptography

    FV-017
    Posted
    Checked

    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.
    Report a problem

  16. Antithesis Software

    Senior/Staff Engineer - Bombadil

    On-site London, UK

    Senior

    • LTL
    • property-based testing
    • Rust
    • testing
    • web applications

    FV-020
    Posted
    Checked

    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.
    Report a problem

  17. Apple Hardware

    Formal Verification Engineer

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

    Engineer

    • SystemVerilog
    • SVA
    • hardware
    • security

    FV-021
    Posted
    Checked

    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.
    Report a problem

  18. Apple Hardware

    Formal Verification Engineer

    On-site Munich, Germany

    Various

    • SVA
    • PSL
    • hardware
    • CPU

    FV-022
    Posted
    Checked

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

  19. Apple Hardware

    GPU Formal Verification Engineer

    On-site Santa Clara, CA

    Engineer

    • SystemVerilog
    • SVA
    • hardware
    • GPU
    • security

    FV-023
    Posted
    Checked

    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.
    Report a problem

  20. 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

    FV-024
    Checked

    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.
    Report a problem

  21. Arm Hardware

    Formal Verification Engineer

    Hybrid Cambridge, United Kingdom

    Senior

    • model checking
    • SystemVerilog
    • hardware
    • CPU

    FV-025
    Posted
    Checked

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

  22. Arm Hardware

    Staff Architecture Formal Engineer

    Hybrid Cambridge, United Kingdom

    Senior

    • OCaml
    • ASL
    • memory model tools
    • hardware
    • ISA specification

    FV-026
    Posted
    Checked

    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.
    Report a problem

  23. Astera Labs Hardware

    Distinguished Formal Verification

    On-site San Jose, CA

    Principal

    • SystemVerilog
    • SVA
    • hardware
    • interconnect
    • AI infrastructure

    FV-028
    Posted
    Checked

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

  24. 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

    FV-029
    Posted
    Checked

    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.
    Report a problem

  25. Astera Labs Hardware

    Senior/ Staff Formal Verification Engineer

    On-site Tel Aviv, Israel

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • interconnect
    • AI infrastructure

    FV-030
    Posted
    Checked

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

  26. Atalanta Software

    Formal Methods Engineer

    On-site Washington, DC

    Senior

    • Lean
    • Z3
    • automated reasoning
    • model checking
    • Rust
    • SMT
    • static analysis
    • theorem proving
    • defense
    • space
    • energy
    • AI for verification
    • hardware
    • software
    • cryptography
    • security
    • AI safety

    FV-144
    Checked

    Pay, eligibility and notes
    Pay
    USD 225,000–275,000 plus equity
    Work authorization
    U.S. citizenship required; must be eligible for a TS/SCI security clearance
    Notes
    Leads the reasoning engine behind Atalanta's Argo platform and serves as PI on US Government-funded research; PhD required.
    Report a problem

  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

    FV-032
    Posted
    Checked

    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.
    Report a problem

  28. Axiomise Hardware

    Graduate Formal Verification Engineer

    On-site Hemel Hempstead, United Kingdom

    Engineer

    • SystemVerilog
    • SVA
    • PSL
    • hardware
    • EDA services

    FV-033
    Posted
    Checked

    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.
    Report a problem

  29. Axiomise Hardware

    Senior Formal Verification Engineer

    On-site Hemel Hempstead, United Kingdom

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • EDA services

    FV-034
    Posted
    Checked

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

  30. Axiomise Hardware

    Staff Formal Verification Engineer

    On-site Hemel Hempstead, UK

    Principal

    • SystemVerilog Assertions
    • PSL
    • theorem proving
    • equivalence checking
    • hardware
    • verification services

    FV-035
    Posted
    Checked

    Pay, eligibility and notes
    Work authorization
    Visa sponsorship "for exceptional candidates"
    Report a problem

  31. 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

    FV-036
    Posted
    Checked

    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.
    Report a problem

  32. Beneficial AI Foundation Software

    AI Safety Research Scientist / Research Engineer (formal verification)

    Remote (worldwide) Anywhere

    Various

    • Lean
    • Verus
    • Rust
    • AI safety
    • cryptography

    FV-037
    Checked

    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.
    Report a problem

  33. Cadence Design Systems Hardware

    Software Engineer I: Jasper R&D

    On-site Belo Horizonte, Brazil

    Engineer

    • Jasper
    • C++
    • EDA tools

    FV-038
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Develops the Jasper formal tool itself, working on formal engines, HDL synthesis and graph modelling.
    Report a problem

  34. Cadence Design Systems Hardware

    Software Engineer II

    On-site Austin, TX

    Engineer

    • Conformal LEC
    • C++
    • EDA tools

    FV-039
    Posted
    Checked

    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.
    Report a problem

  35. 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

    FV-040
    Checked

    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.
    Report a problem

  36. 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

    FV-041
    Posted
    Checked

    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.
    Report a problem

  37. CertiK Cryptocurrency

    Solidity Compiler Frontend Engineer

    Remote US / Remote

    Engineer

    • SMT
    • theorem provers
    • Solidity
    • Java
    • EVM
    • blockchain
    • smart contracts
    • compilers

    FV-042
    Posted
    Checked

    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.
    Report a problem

  38. 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

    FV-043
    Checked

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

  39. 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

    FV-044
    Posted
    Checked

    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.
    Report a problem

  40. 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

    FV-045
    Checked

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

  41. Code Metal Software

    Research Engineer — Formal Methods

    Hybrid Boston, MA

    Research engineer

    • theorem proving
    • SMT
    • program synthesis
    • static analysis
    • compilers
    • embedded

    FV-046
    Posted
    Checked

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

  42. 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

    FV-047
    Checked

    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.
    Report a problem

  43. 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

    FV-048
    Posted
    Checked

    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.
    Report a problem

  44. eleQtron Software

    Compiler Engineer (f/m/d)

    On-site Hamburg or Siegen, Germany

    Engineer

    • LLVM
    • MLIR
    • QIR
    • C++
    • Rust
    • quantum
    • compilers

    FV-049
    Posted
    Checked

    Report a problem

  45. EPFL Academic

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

    On-site Lausanne, Switzerland

    Postdoc

    • Lean
    • numerical analysis
    • AI for mathematics

    FV-050
    Checked

    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.
    Report a problem

  46. 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

    FV-051
    Checked

    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.
    Report a problem

  47. EPFL Academic

    Postdoc: Networked Systems Abstractions Lab (LASeR)

    On-site Lausanne, Switzerland

    Postdoc

    • NetKAT
    • symbolic automata
    • decision procedures
    • theorem proving
    • networking

    FV-052
    Checked

    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.
    Report a problem

  48. 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

    FV-053
    Checked

    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.
    Report a problem

  49. Etched Hardware

    Formal Verification - DV

    On-site San Jose, CA

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • AI accelerators

    FV-054
    Posted
    Checked

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

  50. 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

    FV-055
    Posted
    Checked

    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.
    Report a problem

  51. 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

    FV-056
    Posted
    Checked

    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.
    Report a problem

  52. 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

    FV-057
    Checked

    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).
    Report a problem

  53. Google Hardware

    ASIC Formal Verification Engineer, TPU Compute

    On-site Sunnyvale, CA

    Senior

    • SystemVerilog
    • SVA
    • Jasper
    • VC Formal
    • Questa Formal
    • hardware
    • AI accelerators

    FV-059
    Checked

    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".
    Report a problem

  54. 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

    FV-060
    Checked

    Pay, eligibility and notes
    Notes
    Google's Israel team for custom server chips.
    Report a problem

  55. 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

    FV-061
    Checked

    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.
    Report a problem

  56. Harmonic AI for proof & autoformalization

    Formal Verification Engineer (Aristotle)

    On-site Palo Alto, CA / London, UK

    Engineer

    • Lean
    • AI for mathematics
    • hardware
    • software verification

    FV-062
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Customer-facing; scope properties, run proofs with Aristotle, diagnose failures.
    Report a problem

  57. Harmonic AI for proof & autoformalization

    Research Engineer

    On-site Palo Alto, CA

    Research engineer

    • Lean
    • theorem proving
    • reinforcement learning
    • AI for mathematics
    • theorem proving

    FV-063
    Posted
    Checked

    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.
    Report a problem

  58. 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

    FV-064
    Posted
    Checked

    Report a problem

  59. IBM Hardware

    Formal Verification Engineer

    Hybrid Bangalore, India

    Senior

    • SVA
    • Verilog
    • VHDL
    • Python
    • hardware
    • CPU

    FV-065
    Posted
    Checked

    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.
    Report a problem

  60. 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

    FV-066
    Checked

    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.
    Report a problem

  61. 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

    FV-067
    Checked

    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.
    Report a problem

  62. Intel Hardware

    Formal Verification Engineer

    On-site Haifa / Jerusalem / Petah Tikva, Israel

    Engineer

    • Jasper
    • SVA
    • model checking
    • equivalence checking
    • hardware
    • networking

    FV-068
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Intel Networking (Ethernet) team.
    Report a problem

  63. 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

    FV-069
    Posted
    Checked

    Pay, eligibility and notes
    Pay
    USD 220,920–311,890
    Work authorization
    Position of Trust: extended background investigation required
    Report a problem

  64. 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

    FV-070
    Checked

    Pay, eligibility and notes
    Notes
    New team; no OCaml or functional programming experience required.
    Report a problem

  65. 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

    FV-071
    Posted
    Checked

    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.
    Report a problem

  66. LUBIS EDA Hardware

    Formal Verification Engineer - Professional Level

    Hybrid Kaiserslautern, Germany

    Engineer

    • SVA
    • Jasper
    • VC Formal
    • Questa Formal
    • OneSpin
    • hardware
    • EDA services

    FV-072
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Formal verification consultancy for clients' RTL.
    Report a problem

  67. LUBIS EDA Hardware

    Formal Verification Engineer - Senior Level

    Hybrid Kaiserslautern, Germany

    Senior

    • SVA
    • hardware
    • EDA services

    FV-073
    Posted
    Checked

    Report a problem

  68. LUBIS EDA Hardware

    Manager Formal Verification (m/f/d)

    Hybrid Kaiserslautern, Germany

    Lead

    • SVA
    • hardware
    • EDA services

    FV-074
    Posted
    Checked

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

  69. Marvell Hardware

    Senior Engineer, Logic Equivalence CAD

    On-site Bangalore, India

    Senior

    • logical equivalence checking
    • hardware
    • EDA tools

    FV-075
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    CAD role owning company-wide RTL-to-gate and gate-to-gate equivalence checking flows.
    Report a problem

  70. Math, Inc. AI for proof & autoformalization

    Open applications (verified mathematics)

    Remote (worldwide) Not stated

    Various

    • Lean
    • AI for mathematics
    • autoformalization

    FV-076
    Checked

    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.
    Report a problem

  71. 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

    FV-077
    Checked

    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.
    Report a problem

  72. 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

    FV-078
    Posted
    Checked

    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.
    Report a problem

  73. 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

    FV-079
    Posted
    Checked

    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.
    Report a problem

  74. Mercor AI for proof & autoformalization

    Mathematician Talent Network

    Remote (worldwide) Remote

    Various

    • mathematical proof
    • AI training data
    • AI for mathematics

    FV-149
    Posted
    Checked

    Pay, eligibility and notes
    Pay
    USD 60–80/hour, part-time (15–30 hours/week)
    Work authorization
    Mercor states it cannot support H-1B or STEM OPT candidates
    Notes
    An open application to Mercor's mathematician network rather than a specific opening: experts are matched to future contract projects training and evaluating AI models in mathematics, including proof and theory work. Independent contracting, paid weekly. Unlike Mercor's Lean listing, the posting names no proof assistant.
    Report a problem

  75. Microsoft Software

    Post Doc Researcher (FoSSE, Microsoft Research India)

    On-site Bangalore, India

    Postdoc

    • formal methods
    • static analysis
    • programming languages
    • software engineering
    • code migration

    FV-080
    Posted
    Checked

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

  76. Microsoft Hardware

    Principal Formal Design Verification Engineer

    On-site Bangalore, India

    Principal

    • SystemVerilog
    • SVA
    • hardware
    • cloud
    • interconnect

    FV-082
    Posted
    Checked

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

  77. 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

    FV-083
    Posted
    Checked

    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".
    Report a problem

  78. 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

    FV-084
    Posted
    Checked

    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).
    Report a problem

  79. Microsoft Software

    Senior Researcher - Software Verification - Microsoft Research

    On-site Redmond, WA

    Research scientist

    • SMT
    • automated reasoning
    • program verification
    • systems software
    • AI for verification

    FV-085
    Posted
    Checked

    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).
    Report a problem

  80. 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

    FV-086
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Req 200063310 (posting title is just "Senior Software Engineer"). Same team as req 200063311.
    Report a problem

  81. 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

    FV-087
    Posted
    Checked

    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.
    Report a problem

  82. Mobileye Hardware

    Experienced Formal Verification Engineer

    On-site Haifa, Israel

    Senior

    • JasperGold
    • SystemVerilog
    • hardware
    • automotive
    • autonomous driving

    FV-088
    Checked

    Pay, eligibility and notes
    Notes
    Automated Driving Hardware group; 5+ years of formal verification experience required.
    Report a problem

  83. 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

    FV-089
    Posted
    Checked

    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.
    Report a problem

  84. 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

    FV-090
    Posted
    Checked

    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.
    Report a problem

  85. NVIDIA AI for proof & autoformalization

    AI Compiler Formal Verification Intern

    On-site Zurich, Switzerland

    Intern

    • Lean
    • SMT
    • compilers
    • AI infrastructure

    FV-091
    Posted
    Checked

    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.
    Report a problem

  86. NVIDIA Hardware

    Formal Verification Engineer - New College Grad 2026

    On-site Santa Clara, CA

    Engineer

    • SystemVerilog
    • SVA
    • JasperGold
    • VC Formal
    • hardware
    • GPU
    • CPU

    FV-093
    Posted
    Checked

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

  87. NVIDIA Software

    Senior Compute System Software Engineer

    On-site Bengaluru, India

    Senior

    • Lean 4
    • TLA+
    • Haskell
    • GPU drivers
    • safety-critical software

    FV-094
    Posted
    Checked

    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.
    Report a problem

  88. NVIDIA Hardware

    Senior Formal Verification Engineer

    On-site Santa Clara, CA / Austin, TX

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • GPU

    FV-095
    Posted
    Checked

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

  89. 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

    FV-096
    Posted
    Checked

    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.
    Report a problem

  90. 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

    FV-097
    Posted
    Checked

    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.
    Report a problem

  91. Oath Technologies Software

    Formal Methods Research Engineer

    On-site Berkeley, CA

    Research engineer

    • Lean
    • Coq
    • Isabelle
    • SMT
    • AI safety
    • AI oversight

    FV-098
    Posted
    Checked

    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.
    Report a problem

  92. 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

    FV-100
    Posted
    Checked

    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.
    Report a problem

  93. Pramaana Labs AI for proof & autoformalization

    Research Intern

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

    Intern

    • Lean
    • Coq
    • Isabelle
    • AI for formal reasoning

    FV-101
    Posted
    Checked

    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.
    Report a problem

  94. 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

    FV-102
    Posted
    Checked

    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.
    Report a problem

  95. 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

    FV-103
    Posted
    Checked

    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.
    Report a problem

  96. Qualcomm Hardware

    CPU Formal Verification Engineer

    On-site Santa Clara, CA

    Senior

    • JasperGold
    • VC Formal
    • ACL2
    • HOL
    • hardware
    • CPU

    FV-104
    Posted
    Checked

    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.
    Report a problem

  97. Qualcomm Hardware

    Formal Verification Senior Engineer - Qualcomm, Cambridge, UK

    On-site Cambridge, United Kingdom

    Engineer

    • SystemVerilog
    • SVA
    • JasperGold
    • VC Formal
    • hardware
    • GPU

    FV-105
    Posted
    Checked

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

  98. Qualcomm Hardware

    Senior Staff Formal Verification Engineer

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

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • GPU

    FV-106
    Posted
    Checked

    Pay, eligibility and notes
    Pay
    USD 203,700–305,500
    Notes
    Adreno GPU.
    Report a problem

  99. Quantinuum Software

    Advanced Quantum Compiler Engineer (925)

    Hybrid Broomfield, CO

    Engineer

    • LLVM
    • MLIR
    • QIR
    • Rust
    • C++
    • quantum
    • compilers

    FV-107
    Posted
    Checked

    Pay, eligibility and notes
    Pay
    USD 138,000–173,000
    Work authorization
    US Person required (citizen, green card, refugee or asylee)
    Report a problem

  100. Resolution AI for proof & autoformalization

    Lean Engineer

    Hybrid Berkeley, CA

    Engineer

    • Lean
    • mathlib
    • autoformalization
    • AI safety
    • alignment theory
    • formal mathematics

    FV-108
    Posted
    Checked

    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.
    Report a problem

  101. 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

    FV-109
    Posted
    Checked

    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.
    Report a problem

  102. 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

    FV-110
    Posted
    Checked

    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.
    Report a problem

  103. Runtime Verification Cryptocurrency

    Open applications — verification engineering (K framework)

    Remote Urbana, IL — remote friendly

    Various

    • K framework
    • executable semantics
    • blockchain
    • language semantics

    FV-111
    Checked

    Report a problem

  104. 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

    FV-112
    Checked

    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.
    Report a problem

  105. Samsung Semiconductor (SARC/ACL) Hardware

    Senior Staff Engineer, GPU Design Verification (Formal Verification)

    On-site San Jose, CA

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • GPU

    FV-113
    Posted
    Checked

    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
    Report a problem

  106. Samsung Semiconductor (SARC/ACL) Hardware

    Staff GPU Design Verification Engineer – Formal Verification

    On-site Austin, TX

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • GPU

    FV-114
    Posted
    Checked

    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.
    Report a problem

  107. 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

    FV-115
    Checked

    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.
    Report a problem

  108. 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

    FV-116
    Posted
    Checked

    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.
    Report a problem

  109. 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

    FV-117
    Posted
    Checked

    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.
    Report a problem

  110. SiFive Hardware

    Senior CPU Formal Verification Engineer

    On-site Hyderabad / Bengaluru, India

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • CPU
    • RISC-V

    FV-118
    Posted
    Checked

    Report a problem

  111. SiFive Hardware

    Staff Design Verification Engineer – CPU Core Formal Verification

    On-site Austin, TX / Santa Clara, CA

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • CPU
    • RISC-V

    FV-119
    Posted
    Checked

    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).
    Report a problem

  112. 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

    FV-120
    Posted
    Checked

    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.
    Report a problem

  113. 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

    FV-121
    Checked

    Pay, eligibility and notes
    Notes
    Supervisor Munyque Mittelmann. Apply by email. Deadline 2026-11-15.
    Report a problem

  114. Synopsys Hardware

    Principal Application Engineer, VC Formal

    On-site Bengaluru, India

    Principal

    • VC Formal
    • SVA
    • EDA tools
    • hardware

    FV-122
    Posted
    Checked

    Report a problem

  115. Synopsys Hardware

    Senior Staff Formal Verification Applications Engineer

    On-site Sunnyvale, CA

    Senior

    • VC Formal
    • SVA
    • EDA tools
    • hardware

    FV-123
    Posted
    Checked

    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.
    Report a problem

  116. Tenstorrent Hardware

    Formal Verification Engineer

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

    Senior

    • SystemVerilog
    • SVA
    • hardware
    • CPU
    • RISC-V
    • AI accelerators

    FV-124
    Posted
    Checked

    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.
    Report a problem

  117. 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

    FV-125
    Posted
    Checked

    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.
    Report a problem

  118. 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

    FV-126
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    Six-month engineering internship building an MCP server that exposes Frama-C to an AI agent.
    Report a problem

  119. 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

    FV-127
    Checked

    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.
    Report a problem

  120. Topos Institute Software

    Research Software Engineer [UK-2026-RSE-1]

    On-site Oxford, UK

    Various

    • type theory
    • category theory
    • categorical logic
    • Rust
    • Haskell
    • TypeScript
    • scientific modelling
    • applied category theory
    • research software

    FV-150
    Checked

    Pay, eligibility and notes
    Pay
    GBP 65,000–85,000 depending on level
    Work authorization
    Topos will consider sponsoring UK visas
    Notes
    One posting for two hires on a new research software engineering team at the non-profit's Oxford office, hiring from entry level to experienced. Client-driven work plus CatColab, a Rust and TypeScript platform for modelling in domain-specific categorical logics. Apply by email with a CV and cover letter; applications are reviewed on a rolling basis.
    Report a problem

  121. Trail of Bits Software

    Senior Security Engineer, Research & Engineering (United Kingdom)

    Remote United Kingdom

    Senior

    • Lean
    • Rocq
    • F*
    • Dafny
    • Verus
    • security assurance
    • verified systems

    FV-128
    Posted
    Checked

    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.
    Report a problem

  122. TrustInSoft Software

    AI Engineer

    On-site Paris, France

    Engineer

    • formal methods
    • C
    • OCaml
    • static analysis
    • AI for verification

    FV-129
    Checked

    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.
    Report a problem

  123. 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

    FV-130
    Checked

    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).
    Report a problem

  124. 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

    FV-131
    Checked

    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.
    Report a problem

  125. 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

    FV-132
    Checked

    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.
    Report a problem

  126. 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

    FV-133
    Posted
    Checked

    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.
    Report a problem

  127. 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

    FV-134
    Posted
    Checked

    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).
    Report a problem

  128. 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

    FV-135
    Posted
    Checked

    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.
    Report a problem

  129. Uppsala University Academic

    PhD student — Scalable Verification of Quantum Programs

    On-site Uppsala, Sweden

    PhD

    • program verification
    • automated theorem proving
    • quantum computing

    FV-136
    Posted
    Checked

    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.
    Report a problem

  130. 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

    FV-137
    Posted
    Checked

    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.
    Report a problem

  131. Veridise Cryptocurrency

    Formal Methods Researcher for ZK

    Remote Flexible

    Research scientist

    • Lean
    • Rocq
    • ACL2
    • SMT
    • Rust
    • C++
    • zero-knowledge
    • blockchain security

    FV-138
    Posted
    Checked

    Pay, eligibility and notes
    Notes
    PhD or equivalent professional research experience requested.
    Report a problem

  132. 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

    FV-139
    Posted
    Checked

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

  133. YosysHQ Hardware

    Synthesis or Formal Verification Developer at YosysHQ

    Remote (worldwide) Anywhere

    Engineer

    • Yosys
    • SymbiYosys
    • SAT
    • SMT
    • C++
    • Rust
    • Python
    • EDA tools
    • open source

    FV-140
    Posted
    Checked

    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.
    Report a problem

  134. Zeroth Research Cryptocurrency

    Research Engineer in Applied Cryptography – Zero-Knowledge Model Checking

    Remote (worldwide) Birmingham, UK / remote UK / remote global

    Research engineer

    • Rust
    • arkworks
    • Halo2
    • Plonky3
    • model checking
    • runtime verification
    • zero-knowledge proofs
    • automated reasoning
    • formal methods
    • cryptography
    • zero-knowledge proofs
    • AI safety

    FV-145
    Checked

    Pay, eligibility and notes
    Pay
    GBP 60,000–80,000 for UK residents, adjusted to local market rates elsewhere
    Notes
    Fixed-term until November 2027, funded by ARIA's Safeguarded AI programme. Mostly remote, with periodic meetups in Birmingham.
    Report a problem

  135. Zeroth Research Software

    Research Engineer in Formal Methods – Protocol Synthesis for Multi-agent Systems

    Remote (worldwide) Birmingham, UK / remote UK / remote global

    Research engineer

    • Lean
    • Rust
    • model checking
    • reactive synthesis
    • temporal logic
    • automated reasoning
    • formal methods
    • program verification
    • theorem proving
    • multi-agent systems
    • AI safety
    • cyber-physical systems
    • communication protocols

    FV-146
    Checked

    Pay, eligibility and notes
    Pay
    GBP 60,000–80,000 for UK residents, adjusted to local market rates elsewhere
    Notes
    Fixed-term until August 2027, renewable with the project; funded by ARIA's Scaling Trust programme. Mostly remote, with periodic meetups in Birmingham.
    Report a problem

  136. Zeroth Research AI for proof & autoformalization

    Research Engineer in Machine Learning – Proof Generation for Cyber-physical Systems

    Remote (worldwide) Birmingham, UK / remote UK / remote global

    Various

    • Lean
    • SMT
    • model checking
    • neural network verification
    • reinforcement learning
    • Python
    • automated reasoning
    • theorem proving
    • cyber-physical systems
    • AI safety
    • AI for verification

    FV-147
    Checked

    Pay, eligibility and notes
    Pay
    GBP 60,000–80,000 for UK residents, adjusted to local market rates elsewhere
    Notes
    One posting for two hires: neural certificate learning and LLM-based certificate generation. Fixed-term until November 2027, funded by ARIA's Safeguarded AI programme; mostly remote, with periodic meetups in Birmingham.
    Report a problem
Closed roles (14)

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

  1. 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

    FV-002
    Closed

    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.

  2. 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

    FV-015
    Posted
    Closed

    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.

  3. 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

    FV-016
    Posted
    Closed

    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.

  4. 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

    FV-018
    Posted
    Closed

    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.

  5. Amazon Web Services Software

    Sr. Software Development Engineer, Automated Reasoning Group

    On-site New York, NY

    Senior

    • automated reasoning
    • formal methods
    • AI safety
    • cloud

    FV-019
    Posted
    Closed

    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.

  6. Arm Hardware

    Theorem Proving Engineer

    Hybrid Austin, TX

    Research engineer

    • ACL2
    • SLEC
    • C
    • Verilog
    • hardware
    • CPU
    • floating point

    FV-027
    Posted
    Closed

    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.

  7. Astera Labs Hardware

    Tech Lead, Formal Verification

    On-site Bengaluru, India

    Lead

    • SystemVerilog
    • SVA
    • hardware
    • interconnect
    • AI infrastructure

    FV-031
    Posted
    Closed

  8. Cryspen Software

    Open applications (Rust verification, hax)

    Hybrid France / Germany

    Various

    • hax
    • Rust
    • F*
    • cryptography

    FV-141
    Closed

    Pay, eligibility and notes
    Notes
    No individual postings listed; speculative applications via info@cryspen.com.

  9. 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

    FV-058
    Closed

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

  10. 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

    FV-142
    Closed

    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.

  11. Imandra Software

    Open applications — R&D (automated reasoning)

    Remote Edinburgh / London / Bristol / Austin

    Various

    • OCaml
    • SMT
    • automated reasoning
    • finance
    • automated reasoning

    FV-143
    Closed

  12. Microsoft Hardware

    Principal Design Verification Engineer - Formal

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

    Principal

    • SystemVerilog
    • SVA
    • hardware
    • cloud
    • interconnect

    FV-081
    Posted
    Closed

    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.

  13. 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

    FV-092
    Posted
    Closed

    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.

  14. Oath Technologies Software

    Research Engineer, Tools & Infrastructure

    On-site Berkeley, CA

    Research engineer

    • developer tooling
    • language servers
    • agent scaffolding
    • AI safety
    • developer tools

    FV-099
    Posted
    Closed

    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.