practical fm
1.0.0
如果您在列表上看到不再存在的公司，或者不再使用正式方法，请发送带有解释的拉请请求。如果您当前在工作，或者知道使用正式方法但不在列表中的公司也是如此。请包括网站，GitHub（如果适用），位置和行业。如果公司正在招聘，请包含广告的链接。
| 姓名 | 地点 | 部门 | 来源 |
|---|---|---|---|
| 亚马逊 | 美国 | 电子商务，云计算 | TLA+ Amazon Web服务如何使用正式方法，在Amazon Web服务上使用正式方法， CBMC模型从AWS数据中心检查引导代码， Dafny AWS加密SDK |
| 空客 | 法国 | Astrée ）：“ 2003年，阿斯特雷（Astrée）在空中客车模型的主要飞行控制软件中没有任何运行时错误。该系统的132,000行C代码在仅在2.8GHz 32位PC上使用300mb的300mb使用AMD AMD ATHLON 64使用50分钟的50分钟即可在80分钟内完全自动分析80分钟，然后使用50分钟的空气来使用50分钟的空中群体。 Frama-C为各种飞机系列Coq安全关键软件开发中，包括CAVEAT 。 | |
| 奥尔特兰 | 法国，巴黎 | SPARK贡献者 | |
| 苹果 | 美国加利福尼亚州圣克拉拉谷 | 硬件和软件 | |
| 手臂 | 德克萨斯州奥斯汀和美国加利福尼亚州圣何塞 | 硬件 | ACL2验证算术硬件，验证官方手臂规格， TLA+ Linux内核 |
| Adacore | 美国，纽约 | ？ | ？ |
| Alacris | ？ | 区块链 | |
| BAE系统 | Coq reddit | ||
| 基岩系统 | 美国波士顿和湾区；德国柏林和慕尼黑 | 系统安全，值得信赖的计算 | Coq ， C++ ，GitHub |
| 波音公司 | 美国 | 航空航天，防御 | Coq （无证明）， Ivory （来源） |
| 博世 | 德国 | 汽车 | 阿斯特雷 |
| 半人造技术 | 美国 | 硬件 | ACL2 |
| COG系统 | 澳大利亚，新南威尔士州，悉尼 | 地点 | |
| 数据61 | 澳大利亚 | Isabelle/HOL （SEL4验证项目） | |
| 德雷珀 | 美国 | 防御，空间 | Coq ， Z3 |
| 以太坊 | 瑞士 | Why3 DEV更新：正式方法， Isabelle/HOL A LEM对EVM和一些Isabelle/HOL证明， Coq对以太坊合同的正式验证 | |
| edgeSecurity | 软件 | Tamarin林士兵 | |
| Espark学习 | 美国，伊利诺伊州，芝加哥 | 教育 | 实践中TLA+正式方法：在Espark学习中使用TLA+ |
| 松紧带 | 全球的 | 搜索和分析软件 | TLA+ Isabelle/HOL Elasticsearch-Formal-Models存储库会议和当前的开放位置 |
| 欧洲航天局 | TLA+ （以网络为中心的RTO的正式开发： 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+ | ||
| 美国 | INFER使用软件验证Zoncolan快速移动，Facebook如何使用静态分析来检测和防止安全问题 | ||
| 火EEYE | 德累斯顿，德国（团队已倒闭） | 安全 | Coq职位公告：FireEye的正式方法工程师和科学开发人员 |
| 防鳍 | 俄罗斯，股东 | 金融（区块链） | Coq ， Agda |
| 正式土地 | 全球的 | 软件 | Tezos区块链的Coq验证 |
| 正式辩护 | 西班牙巴塞罗那 | 法律 | Coq正式DateTime软件 |
| 加洛伊斯 | 美国俄勒冈州波特兰 | 咨询/研究 | Coq （？） |
| funa gmbh | 德国 | CPAchecker软件质量的另一道路？自动化软件验证和OpenBSD以及软件验证的应用到OpenBSD网络模块 | |
| 谷歌 | 美国CA | 云计算，计算机软件，AI | Coq （密码算术的简单高级代码 - 具有证据，没有折衷（铬）），实时Maude的Google Megastore的正式建模和分析 |
| Grammatech | Frama-C c库图书馆注释for frama-c：经验报告 | ||
| Green Hills软件 | 美国 | 航天 | ACL2 ACL2的工业用途 |
| Kestrel Institute | 美国 | 计算机科学研究 | 主要是ACL2，一些Isabelle/Hol，一点点PV和COQ。有关详细信息和出版物，请参见网站，尤其是项目页面和人员页面。 |
| IBM | 美国 | ？ | SPIN/Promela Paul E. McKenney's Journal，从根本上讲RCU是什么？ （Linux内核，RCU）， Coq Q*CERT |
| IgE+XAO | 欧洲 | 计算机辅助设计 | 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 （自定义语言类型推理）（v）小型研究项目 |
| 英特尔 | 美国 | 硬件 | Prover （在英特尔进行了15年的正式财产验证）， HOL Light （IA-64部门算法的正式验证）， TLA+ （RTL Pre-RTL正式验证：Intel经验） |
| 非正式系统 | 多伦多，维也纳，洛桑，柏林 | 区块链，分布式系统 | TLA+ APALACHE，TLA+的符号模型检查器， Rust Tendermint BFT共识和Interblockchain通信协议与TLA+ Specs，使用TLA+和Apalache进行基于模型的测试 |
| Infotecs | 俄罗斯，莫斯科 | TLA+ ， Coq ，构造和正式验证易于故障分布的相互排除算法，построениениекри至¢ | |
| ISP RAS | 俄罗斯莫斯科 | 操作系统；硬件 | Frama-C ， Jessie ， Why3 Astraver，Linux内核库的功能正式验证； SPIN/Promela ， Microtesk网站； Event-B电电电仑函CAP9内核的Isabelle/HOL正式规范 |
| Kernkonzept GmbH | 德国 | 操作系统 | L4Re （来源） |
| 卡巴斯基 | 俄罗斯莫斯科 | 安全/AV | 合金，TLA， Event-B （源）， Ivory （源） |
| 机器区域Inc. | 俄罗斯 | 移动游戏软件，实时计算，基于云的网络 | TLA+ Twitter |
| 微软 | 美国雷德蒙德 | 软件开发 | TLA+ TLA+证明，对程序员的思考，Azure Cosmos DB提供的五个一致性水平的高级TLA+规格， Microsoft's Static Driver Verifier彻底对设备驱动程序的静态静态分析Clousot静态分析，使用抽象的解释，正式的方法和工具，用于分布式系统，分布式系统，在Microsoft中进行正式方法 |
| mongodb | 美国纽约 | 软件开发 | MongoDB复制系统简化部分的TLA+ TLA+规格 |
| NASA | 美国 | 空间 | PVS NASA Langley正式方法研究计划。 JPF Java Pathfinder，强大的软件工程组， Model Checking喷气推进实验室， SPIN/Promela启发性旋转， PVS （来源） |
| 游牧实验室 | 法国巴黎 | 区块链 | 有关软件验证的Coq页面 |
| Oracle | 美国加利福尼亚州雷德伍德海岸 | 企业软件，云计算，计算机硬件 | ACL2 （证明有关Java和ACL2的JVM的定理） |
| 特定软件 | NServiceBus的TLA+ TLA+规格 | ||
| pingcap | TIDB中的TLA+ TLA+ | ||
| 供者技术 | 欧洲 | 铁路 | Model checking |
| rusbitech（с可） | 俄罗斯，莫斯科 | Системное ПО | Frama-C ， Event-B （截约 |
| 罗克韦尔·柯林斯（Rockwell Collins） | 美国，爱荷华州雪松急流 | 高保证系统 | 航空航天行业的正式方法：遵循这笔钱 |
| Serokell | 塔林，爱沙尼亚 | 金融科技，区块链，物联网，机器学习，正式验证 | Agda |
| 概要 | ？ | ？ | 地点 |
| Systerel | 法国 | 软件，咨询，服务 | S3 A模型检查器，用于同步语言，B方法，事件B/Rodin。招募。 |
| sifive | 美国，旧金山湾地区 | 硬件 | Coq LinkedIn |
| 状态框 | 阿姆斯特丹，荷兰 | 区块链 | Idris （github） |
| Sukhoi | 俄罗斯，莫斯科 | 航空航天和防御 | ANSYS SCADE Suite （来源 - 正式验证的luster编译器） |
| Thales | Frama-C （通用标准认证的自下而上的正式验证方法：适用于Javacard虚拟机） | ||
| Trustinsoft | 美国加利福尼亚州，旧金山 | - | TrustInSoft Analyzer网站 |
| 值得信赖的系统 | 澳大利亚，悉尼 | Isabelle/HOL ， Coq网站 | |
| 两个六个技术 | 美国 | 国防研究 | Isabelle/HOL ，硬件验证（示例）， Coq （示例） |
| Jetbrains Research | 俄罗斯圣彼得堡 | - | Coq （来源） |
| 歌 | 俄罗斯莫斯科 | ？ | SPIN/Promela |
| T平台 | 俄罗斯莫斯科 | - | Coq ， SPIN/Promela ， TLA+ ， McErlang ， mCRL2员工CV |
| 库恩 | 瑞士吉夫 | CERN大型强子对撞机的CMS实验的mCRL2控制软件 | |
| yandex | 软件 | TLA+ ClickHouse复制算法，无锁存储器分配器 | |
| Zilliqa | 新加坡 | 区块链 | Coq Scilla-COQ项目 |
| 波浪 | 区块链 | ??? |
