Amazon |
USA |
eCommerce, Cloud computing |
TLA+ How Amazon Web Services Uses Formal Methods, Use of Formal Methods at Amazon Web Services |
Airbus |
France |
|
Astr ́ee , Coq Interview with Xavier Leroy |
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 |
? |
? |
BAE Systems |
|
|
Coq Reddit |
The Boeing Company |
USA |
Aerospace, Defense |
Coq (no proof) |
Centaur Technology |
USA |
Hardware |
ACL2 |
Cog Systems |
Australia, New South Wales, Sydney |
|
Site |
Data61 |
Australia |
|
Isabelle/HOL (seL4) |
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 |
FireEye |
Dresden, Germany (team defunct) |
Security |
Coq Job announcement: formal methods engineer and scientific developer at FireEye |
Galois |
Portland, Oregon, USA |
Consulting/Research |
Coq (?) |
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 |
[Fifteen Years of Formal Property Verification in Intel]q(https://link.springer.com/chapter/10.1007%2F978-3-540-69850-0_8?LI=true) |
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; SPIN/Promela , Microtesk Site |
Kernkonzept |
Germany |
Operating systems |
Site |
Kaspersky Lab |
Moscow, Russia |
Security/AV |
Что представляет собой операционная система Kaspesky OS? |
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 |
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. |
PingCAP |
|
|
TLA+ TLA+ in TiDB |
Rockwell Collins |
USA, Cedar Rapids, Iowa |
High Assurance Systems |
? |
Synopsis |
? |
? |
Site |
SiFive |
USA, San Francisco Bay Area |
Hardware |
Coq LinkedIn |
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 |
Ziliqa |
? |
Blockchain |
Coq |