Skip to content

A gently curated list of companies using verification formal methods in industry

Notifications You must be signed in to change notification settings

ligurio/practical-fm

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

95 Commits
 
 

Repository files navigation

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