A List of companies that use formal verification methods in software engineering

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, CBMC Model Checking Boot Code from AWS Data Centers
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 vari­ous plane series, including the A380.", Coq (Interview with Xavier Leroy), CAVEAT, a C-verifier developed by CEA and used by Airbus.
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 (The seL4 verification project)
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
Facebook	USA		INFER Moving Fast with Software Verification Zoncolan How Facebook uses static analysis to detect and prevent security issues
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 (?)
Google	CA, USA	Cloud computing, Computer software, AI	Coq (Simple High-Level Code For Cryptographic Arithmetic – With Proofs, Without Compromises (Chromium))
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	Prover (Fifteen Years of Formal Property Verification in Intel), HOL Light (Formal verification of IA-64 division algorithms)
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, Linux kernel library functions formally verified; SPIN/Promela, Microtesk Site; Event-B Моделирование и верификация политик безопасности управления доступом в операционных системах, part of the Event-B specification; Isabelle/HOL Formal specification of the Cap9 kernel
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 Clousot Static contrace checking with Abstract Interpretation
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)
Oracle	Redwood Shores, CA, USA	Enterprise software, Cloud computing, Computer hardware	ACL2 (Proving Theorems about Java and the JVM with ACL2)
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
Systerel	France	Software, Consulting, Service	S3 a model checker for a synchrone language, B method, Event-b/Rodin. Recruiting.
SiFive	USA, San Francisco Bay Area	Hardware	Coq LinkedIn
Statebox	Amsterdam, Netherlands	Blockchain	Idris (github)
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
Zilliqa	Singapore	Blockchain	Coq scilla-coq project

See also

• Formal Methods Companies (outdated)
• Open vacancies on indeed.com
• Formal Methods: Practice and Experience
• http://alloytools.org/citations/case-studies.html
• Overview of formal methods in software engineering
• TLA+ http://lamport.azurewebsites.net/tla/industrial-use.html
• TLA+ https://news.ycombinator.com/item?id=9601770