Need help with practical-fm?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

ligurio
330 Stars 28 Forks 83 Commits 2 Opened issues

Description

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

Services available

!
?

Need anything else?

Contributors list

# 6,041
coq
tla
SQLite
unix
50 commits
# 306,251
coq
OCaml
Shell
sed
3 commits
# 79,570
Objecti...
coq
carthag...
cocoapo...
2 commits
# 200,215
Redis
Rails
postgre...
formal-...
2 commits
# 362,760
Shell
formal-...
coq
reprodu...
2 commits
# 384,123
OCaml
Shell
formal-...
formal-...
1 commit
# 605,855
formal-...
formal-...
coq
1 commit
# 484,610
Haskell
Shell
formal-...
formal-...
1 commit
# 10,579
Go
Shell
proof-o...
coq
1 commit
# 205,504
idris
formal-...
categor...
Shell
1 commit
# 170,130
coq
Shell
Emacs
idris
1 commit
# 581,450
formal-...
formal-...
coq
1 commit

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 | 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
|
ACL2
[Industrial Use of 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 Vindications | Barcelona, Spain | Law |
Coq
Philosophy presentation 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 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 Lab | Moscow, Russia | Security/AV | Что представляет собой операционная система Kaspesky OS?,
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 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) TrustInSoft | USA, CA, San Francisco | - |
TrustInSoft Analyzer
Site Trustworthy Systems | Australia, Sydney | |
Isabelle/HOL
,
Coq
Site 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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.