Skip to content
/ practical-fm Public
forked from ligurio/practical-fm

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

0 stars 38 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

matclab/practical-fm

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

58 Commits
README.md
README.md
 
 

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
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
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

About

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

Resources

Readme
Activity

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published