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項目 |
| 波浪 | 區塊鏈 | ??? |
