• Stars
    star
    456
  • Rank 95,985 (Top 2 %)
  • Language
  • Created over 6 years ago
  • Updated 8 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

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

More Repositories

1

awesome-ci

List of Continuous Integration services
3,453
star
2

sqa-wiki

My own notes (drafts mostly) about software quality
2,213
star
3

awesome-ttygames

Unix ASCII games
HTML
758
star
4

awesome-openbsd

A curated list of awesome OpenBSD resources
424
star
5

unreliablefs

A FUSE-based fault injection filesystem.
C
170
star
6

openbsd-cookbooks

Setup environment in OpenBSD using Ansible playbook
Shell
88
star
7

swebok-2004-in-russian

Основы программной инженерии (SWEBOK 2004 на русском) в EPUB и HTML
Makefile
59
star
8

lark-grammars

Grammars suitable for lark parser and Hypothesis
Python
40
star
9

luzer

A coverage-guided, native Lua fuzzing engine.
C
34
star
10

swebok-v3

Guide to the Software Engineering Body of Knowledge Version 3 (SWEBOK)
Makefile
24
star
11

open-history-data

Поиск людей из прошлого
Python
24
star
12

elle-cli

command-line frontend to transactional consistency checkers for black-box databases
Clojure
23
star
13

openbsd-tests

Unofficial OpenBSD regression tests
Jupyter Notebook
22
star
14

clojure-from-the-ground-up

Book about Clojure written by Kyle Kingsbury https://aphyr.com/tags/Clojure-from-the-ground-up, formatting and conversion to Markdown, EPUB and HTML by Sergey Bronnikov.
CSS
18
star
15

gromit

EBNF grammar fuzzer
Go
17
star
16

lua-c-manual-pages

Lua 5.1 C API manual pages
Roff
15
star
17

jenny

Tool for generating regression tests
C
14
star
18

git-test

Run automated tests against a range of Git commits and keep track of the results
Shell
13
star
19

semgrep-rules

semgrep rules for flakiness, missed error handling, Lua antipatterns and pitfalls.
Lua
12
star
20

gedcom

Genealogy Tools
Jupyter Notebook
10
star
21

lua-c-api-tests

Lua C API tests
C++
9
star
22

molly

Framework for distributed system's verification, with fault injection.
Lua
9
star
23

parallels-plesk-dockefile

Dockefile for Parallels Plesk Panel
Shell
7
star
24

testres-db

is a tool to import test results into SQLite database
Go
7
star
25

planet-openbsd

Planet OpenBSD
CSS
7
star
26

py-mutation-testing-elements

Generator of HTML reports with mutation testing results
Python
6
star
27

packetdrill-testcases

packetdrill testcases for network regression testing
Python
5
star
28

berkeley-db.1.85

This is version 1.85 of the Berkeley DB code.
C
5
star
29

zabbix-virtuozzo-template

Zabbix template for Virtuozzo
5
star
30

pg_feedback

PostgreSQL Feedback Plugin
C
5
star
31

go-contracts

A draft implementation of contracts for Golang ("require no more, promise no less")
Go
4
star
32

twisource

OpenVZ tweets
Go
4
star
33

testres

A hyperfast web frontend for software testing results written in C.
C
4
star
34

afl-lua

Integration of AFL (American Fuzzy Lop) with Lua programming language. Superseded by https://github.com/ligurio/luzer.
C
3
star
35

lua-c-api-corpus

Lua C API seed corpus
3
star
36

wwwc

Board engine written in C++
C++
3
star
37

blog

My blog / Мой блог
HTML
3
star
38

litclock

is a clock using time quotes from literature
HTML
3
star
39

snippets

My experiments and snippets
HTML
2
star
40

runmap

Беговые дорожки Москвы 🏃
CSS
2
star
41

ligurio

2
star
42

openvz-playbooks

Ansible playbooks/files/etc repository for OpenVZ infrastructure
PHP
2
star
43

openvz-packer-templates

Vagrant boxes for Virtuozzo and OpenVZ
Shell
2
star
44

postgresql-perf-tools

PostgreSQL Performance Monitoring Tools
Python
2
star
45

runtest

runtest - is a program for running OpenBSD regression tests.
C
2
star
46

pg-tests

Mirror of https://git.postgrespro.ru/automation/pg-tests
Python
2
star
47

race-number-tagger

Machine learning model to detect race numbers
Python
1
star
48

openbsd-wip

OpenBSD work in progress ports
Makefile
1
star
49

mulua

A practical mutation testing tool for Lua.
1
star
50

report-samples

Samples of testing and code coverage reports
Raku
1
star
51

go-cobertura

Cobertura XML format parser for the Go programming language
Go
1
star
52

molly-tests

Lua
1
star