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, Dafny AWS Encryption SDK
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., Frama-C (Industrial use of a safe and efficient formal method based software engineering process in avionics).
Altran	France, Paris		SPARK SPARK contributors
Apple	Santa Clara Valley, California, USA	Hardware and Software
Arm	Austin, Texas, & San Jose, California, USA	Hardware	ACL2 Verification of Arithmetic Hardware, Verifying against the official ARM specification, TLA+ Linux Kernel
AdaCore	USA, New York	?	?
Alacris	?	Blockchain
BAE Systems			Coq Reddit
BedRock Systems	Boston & Bay Area, USA; Berlin & Munich, Germany	Systems Security, Trustworthy Compute	Coq, C++, github
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)
Draper	USA	Defense, Space	Coq, Z3
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
EdgeSecurity		Software	Tamarin WireGuard
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
European Space Agency			TLA+ (Formal Development of a Network-Centric RTOS: The European Space Agency's Rosetta spacecraft, which flew to a comet, used a real-time operating system called Virtuoso to control some of its instruments. The next version of that operating system, called OpenComRTOS, was developed using TLA+)
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
Formal Land	Global	Software	Coq Verification of the Tezos blockchain
Formal Vindications	Barcelona, Spain	Law	Coq Formalized datetime software
Galois	Portland, Oregon, USA	Consulting/Research	Coq (?)
genua GmbH	Germany		CPAchecker Another Path for Software Quality? Automated Software Verification and OpenBSD and Application of Software Verificationto OpenBSD Network Modules
Google	CA, USA	Cloud computing, Computer software, AI	Coq (Simple High-Level Code For Cryptographic Arithmetic – With Proofs, Without Compromises (Chromium)), Formal Modeling and Analysis of Google’s Megastore in Real-Time Maude
Grammatech			Frama-C C Library annotations in ACSL for Frama-C: experience report
Green Hills Software	USA	Aerospace	ACL2 Industrial Use of ACL2
Kestrel Institute	USA	Computer Science Research	Mostly ACL2, some Isabelle/HOL, a little of PVS and Coq. See the web site, particularly project pages and people pages, for details and publications.
IBM	USA	?	SPIN/Promela Paul E. McKenney's Journal, What is RCU, Fundamentally? (Linux Kernel, RCU), Coq Q*Cert
IGE+XAO	Europe	Computer Aided Design	Coq Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context Coq is used to verify the following: (i) domain-specific algorithms (application of "patches" to electrical design documents) (ii) graph algorithms (A* search, length-preserving tree layout, B&B TSP, ...) (iii) data structures (union-find, priority queues, ...) (iv) programming language related questions (custom language type inference) (v) small research projects
Intel	USA	Hardware	Prover (Fifteen Years of Formal Property Verification in Intel), HOL Light (Formal verification of IA-64 division algorithms), TLA+ (Pre-RTL formal Verification: An Intel Experience)
Informal Systems	Toronto, Vienna, Lausanne, Berlin	Blockchain, Distributed Systems	TLA+ Apalache, Symbolic Model Checker for TLA+, Rust Tendermint BFT Consensus and Interblockchain Communication protocol in Rust with TLA+ specs, Model Based Testing with TLA+ and Apalache
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 GmbH	Germany	Operating systems	L4Re (source)
Kaspersky	Moscow, Russia	Security/AV	Alloy, TLA, Event-B (source), 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, Formal Methods and Tools for Distributed Systems, Formal Methods at Scale in Microsoft
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)
Nomadic Labs	Paris, France	blockchain	Coq page on software verification
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
Prover Technology	Europe	Railway	Model checking
Rusbitech (РусБиТех)	Russia, Moscow	Системное ПО	Frama-C, Event-B (Моделирование и верификация политик безопасности управления доступом в операционных системах)
Rockwell Collins	USA, Cedar Rapids, Iowa	High Assurance Systems	Formal Methods in the Aerospace Industry: Follow the Money
Serokell	Tallinn, Estonia	Fintech, blockchain, IoT, machine learning, formal verification	Agda
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)
Thales			Frama-C (A Bottom-Up Formal Verification Approach for Common Criteria Certification: Application to JavaCard Virtual Machine)
TrustInSoft	USA, CA, San Francisco	-	TrustInSoft Analyzer Site
Trustworthy Systems	Australia, Sydney		Isabelle/HOL, Coq Site
Two Six Technologies	USA	Defense research	Isabelle/HOL, Hardware verification (example), Coq (example)
JetBrains Research	Saint Petersburg, Russia	-	Coq (source)
МЦСТ	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
Yandex		Software	TLA+ ClickHouse Replication Algorithm, lock-free Memory Allocator
Zilliqa	Singapore	Blockchain	Coq scilla-coq project
Waves		Blockchain	???

See also

• Formal Methods Companies (outdated)
• Open vacancies on indeed.com
• Formal Methods: Practice and Experience - Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John Fitzgerald
• http://alloytools.org/citations/case-studies.html
• Overview of formal methods in software engineering
• TLA+ https://news.ycombinator.com/item?id=9601770
• System specifications written in Promela