If you see a company on the list that doesn't exist anymore, or does not use formal methods anymore, please send a pull request with an explanation. The same goes if you're currently working at, or know a company that uses formal methods but is not on the list. Please include the website, github (if applicable), locations, and sector. If the company is hiring please include a link to the ad.
| Name | Location | Sector | Source |
|---|---|---|---|
| Amazon | USA | eCommerce, Cloud computing | TLA+ How Amazon Web Services Uses Formal Methods, Use of Formal Methods at Amazon Web Services |
| Airbus | France | Astrée: "In 2003, Astrée proved the absence of any runtime errors in the primary flight-control software of an Airbus model. The system’s 132,000 lines of C code were analyzed completely automatically in only 80 minutes on a 2.8GHz 32-bit PC using 300MB of memory (and in only 50 minutes on an AMD Athlon 64 using 580MB of memory). Since then, Airbus France has been using Astrée in the development of safety-critical software for various plane series, including the A380.", Coq (Interview with Xavier Leroy) |
|
| Altran | France, Paris | SPARK SPARK contributors |
|
| Apple | Santa Clara Valley, California, USA | Hardware and Software | |
| ARM | USA, California, San Jose | Hardware | Verifying against the official ARM specification, TLA+ Linux Kernel |
| AdaCore | USA, New York | ? | ? |
| Alacris | ? | Blockchain | |
| BAE Systems | Coq Reddit |
||
| Bedrock Systems | USA, Menlo Park, CA | ? | ? |
| The Boeing Company | USA | Aerospace, Defense | Coq (no proof), Ivory (source) |
| Bosch | Germany | Automotive | Astrée |
| Centaur Technology | USA | Hardware | ACL2 |
| Cog Systems | Australia, New South Wales, Sydney | Site | |
| Data61 | Australia | Isabelle/HOL (seL4) |
|
| Ethereum | Switzerland | Why3 Dev Update: Formal Methods, Isabelle/HOL A Lem formalization of EVM and some Isabelle/HOL proofs, Coq Formal Verification of Ethereum Contracts |
|
| eSpark Learning | USA, IL, Chicago | Education | TLA+ Formal Methods in Practice: Using TLA+ at eSpark Learning |
| Elastic | Global | Search & analytics software | TLA+ Isabelle/HOL elasticsearch-formal-models repository conference talk and current open positions |
| USA | INFER Moving Fast with Software Verification |
||
| FireEye | Dresden, Germany (team defunct) | Security | Coq Job announcement: formal methods engineer and scientific developer at FireEye |
| FinProof | Russia, SPb | Finance (Blockchain) | Coq, Agda |
| Galois | Portland, Oregon, USA | Consulting/Research | Coq (?) |
| Grammatech | Frama-C C Library annotations in ACSL for Frama-C: experience report |
||
| Green Hills Software | USA | Aerospace | ACL2 Industrial Use of ACL2 |
| IBM | USA | ? | SPIN/Promela Paul E. McKenney's Journal, What is RCU, Fundamentally? (Linux Kernel, RCU) |
| Intel | USA | Hardware | Fifteen Years of Formal Property Verification in Intel |
| InfoTecs | Russia, Moscow | TLA+, Coq, Construction and formal verification of a fault-tolerant distributed mutual exclusion algorithm, Построение и верификация отказоустойчивого алгоритма распределенной блокировки |
|
| ISP RAS | Moscow, Russia | Operating systems; hardware | Frama-C, Jessie, Why3 Astraver; SPIN/Promela, Microtesk Site |
| Kernkonzept | Germany | Operating systems | Site |
| Kaspersky Lab | Moscow, Russia | Security/AV | Что представляет собой операционная система Kaspesky OS?, Ivory (source) |
| Machine Zone Inc. | Russia | Mobile gaming software, Real-time computing, Cloud-based networking | TLA+ Twitter |
| Microsoft | Redmond, USA | Software development | TLA+ TLA+ Proofs, Thinking for Programmers, High-level TLA+ specifications for the five consistency levels offered by Azure Cosmos DB, Microsoft’s Static Driver Verifier Thorough static analysis of device drivers |
| MongoDB | New York, USA | Software development | TLA+ TLA+ Spec of a simplified part of MongoDB replication system |
| NASA | USA | Space | PVS NASA Langley Formal Methods Research Program. JPF Java Pathfinder, Robust Software Engineering Group, Model Checking Jet Propulsion Laboratory, SPIN/Promela Inspiring Applications of Spin, PVS (source) |
| Particular Software | TLA+ TLA+ Specifications for NServiceBus |
||
| PingCAP | TLA+ TLA+ in TiDB |
||
| Rockwell Collins | USA, Cedar Rapids, Iowa | High Assurance Systems | Formal Methods in the Aerospace Industry: Follow the Money |
| Synopsis | ? | ? | Site |
| SiFive | USA, San Francisco Bay Area | Hardware | Coq LinkedIn |
| Sukhoi | Russia, Moscow | Aerospace and defense | ANSYS SCADE Suite (source - A Formally Verified Compiler for Lustre) |
| TrustInSoft | USA, CA, San Francisco | - | TrustInSoft Analyzer Site |
| Trustworthy Systems | Australia, Sydney | Isabelle/HOL, Coq Site |
|
| JetBrains | Saint Petersburg, Russia | - | Site |
| МЦСТ | Moscow, Russia | ? | SPIN/Promela Методы и средства верификации протоколов когерентности памяти |
| T-Platforms | Moscow, Russia | - | Coq, SPIN/Promela, TLA+, McErlang, mCRL2 Employee CV |
| CERN | Genève, Switzerland | mCRL2 Control Software of the CMS Experiment at CERN’s Large Hadron Collider |
|
| Ziliqa | ? | Blockchain | Coq |
- Formal Methods Companies (outdated)
- Open vacancies on indeed.com
- Formal Methods: Practice and Experience