practical fm
1.0.0
リストに存在しなくなった、または正式な方法を使用しない会社が表示されている場合は、説明とともにプルリクエストを送信してください。現在働いている場合、または正式な方法を使用しているがリストに載っていない会社を知っている場合、同じことが言えます。 Webサイト、Github（該当する場合）、場所、およびセクターを含めてください。会社が雇用している場合は、広告へのリンクを含めてください。
| 名前 | 位置 | セクタ | ソース |
|---|---|---|---|
| アマゾン | アメリカ合衆国 | eコマース、クラウドコンピューティング | TLA+ Amazon Web Servicesが正式な方法、Amazon Webサービスでの正式な方法の使用、AWSデータセンターのCBMCモデルチェックブートコード、 Dafny暗号化SDK |
| エアバス | フランス | Astrée ：「2003年、Astreeはエアバスモデルのプライマリフライトコントロールソフトウェアにランタイムエラーがないことを証明しました。システムの132,000行のCコードは、300MBのメモリを使用して（およびAMD ATHLANCEを使用して50分で50分で50分で50分で、2.8GHz 32ビットPCでわずか80分で完全に自動的に分析されました。 A380を含むさまざまな飛行機シリーズ用の安全性が批判的なソフトウェア。」、 Coq （Xavier Leroyとのインタビュー）、 CAVEAT 、CEAが開発し、Airbus。が使用するC Frama-C Verifier。 | |
| アルトラン | フランス、パリ | SPARK Sparkの貢献者 | |
| りんご | サンタクララバレー、カリフォルニア、米国 | ハードウェアとソフトウェア | |
| アーム | テキサス州オースティン、および米国カリフォルニア州サンノゼ | ハードウェア | 算術ハードウェアのACL2検証、公式のアーム仕様に対する検証、 TLA+ Linuxカーネル |
| アダコア | 米国、ニューヨーク | ？ | ？ |
| アラクリス | ？ | ブロックチェーン | |
| BAEシステム | Coq reddit | ||
| 岩盤システム | 米国ボストン＆ベイエリア;ベルリン＆ミュンヘン、ドイツ | システムセキュリティ、信頼できる計算 | Coq 、 C++ 、github |
| ボーイングカンパニー | アメリカ合衆国 | 航空宇宙、防衛 | Coq （証明なし）、 Ivory （ソース） |
| ボッシュ | ドイツ | 自動車 | アストレ |
| Centaurテクノロジー | アメリカ合衆国 | ハードウェア | ACL2 |
| コグシステム | オーストラリア、ニューサウスウェールズ、シドニー | サイト | |
| data61 | オーストラリア | Isabelle/HOL （SEL4検証プロジェクト） | |
| ドレーパー | アメリカ合衆国 | 防衛、スペース | Coq 、 Z3 |
| イーサリアム | スイス | Why3 Dev Update：正式な方法、 Isabelle/HOL eVMおよびいくつかのイザベル/ホルプルーフの形式化、イーサリアム契約のCoqな検証 | |
| エッジセキュリティ | ソフトウェア | Tamarinワイヤーガード | |
| Espark Learning | 米国、イリノイ州、シカゴ | 教育 | TLA+正式な方法実際に：ESPARK Learningで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+ | ||
| アメリカ合衆国 | ソフトウェア検証で速く移動するZoncolan Facebookが静的分析を使用してセキュリティの問題を検出および防止する方法をINFERする | ||
| Fireeye | ドイツ、ドレスデン（チームの廃止） | 安全 | Coqジョブの発表：Fireeyeの正式な方法エンジニアおよび科学開発者 |
| フィンプルーフ | ロシア、SPB | 金融（ブロックチェーン） | Coq 、 Agda |
| 正式な土地 | グローバル | ソフトウェア | TezosブロックチェーンのCoq検証 |
| 正式な立証 | スペイン、バルセロナ | 法 | Coq正式化されたDateTimeソフトウェア |
| ガロア | 米国オレゴン州ポートランド | コンサルティング/調査 | Coq （？） |
| gena gmbh | ドイツ | CPAcheckerソフトウェア品質の別のパス？自動化されたソフトウェア検証とOpenBSDおよびソフトウェア検証のアプリケーションOpenBSDネットワークモジュール | |
| グーグル | 米国CA | クラウドコンピューティング、コンピューターソフトウェア、AI | Coq （暗号化算術のための単純な高レベルコード - 妥協のない証明を備えた（クロム））、Googleのメガストーレの正式なモデリングと分析 |
| Grammatech | Frama-C c frama-cのACSLでの図書館注釈：経験レポート | ||
| グリーンヒルズソフトウェア | アメリカ合衆国 | 航空宇宙 | ACL2 ACL2の産業用使用 |
| ケストレル研究所 | アメリカ合衆国 | コンピューターサイエンスの研究 | 主にACL2、いくつかのイザベル/ホル、PVSとCOQの少し。詳細と出版物については、Webサイト、特にプロジェクトページとPeopleページを参照してください。 |
| IBM | アメリカ合衆国 | ？ | SPIN/Promela Paul E. McKenneyのジャーナル、RCUとは基本的には何ですか？ （Linux Kernel、RCU）、 Coq q*cert |
| Ige+Xao | ヨーロッパ | コンピューター支援デザイン | Coq Experienceレポート：CAD開発コンテキスト内のCOQの少し密輸COQは、次の検証に使用されます。 （カスタム言語タイプの推論）（v）小規模な研究プロジェクト |
| インテル | アメリカ合衆国 | ハードウェア | Prover （Intelの15年の正式な財産検証）、 HOL Light （IA-64分割アルゴリズムの正式な検証）、 TLA+ （PRE-RTL正式な検証：Intel Experience） |
| 非公式システム | トロント、ウィーン、ローザンヌ、ベルリン | ブロックチェーン、分散システム | TLA+ Apalache、TLA+のシンボリックモデルチェッカー、TLA+仕様を使用したRustのRust Tendermint BFTコンセンサスおよびインターブロックチェーン通信プロトコル、TLA+およびApalacheによるモデルベースのテスト |
| infotecs | モスクワ、ロシア | TLA+ 、 Coq 、TTLA+、断層耐性分布相互除外アルゴリズムの建設と正式な検証、построениеиверириривここйч | |
| ISP ras | モスクワ、ロシア | オペレーティングシステム;ハードウェア | Frama-C 、 Jessie 、 Why3 Astraver、Linuxカーネルライブラリは正式に検証された機能。 SPIN/Promela 、 Microteskサイト。 Event-B полититиetheзопасностиоправлениядо富用語用語。 CAP9カーネルのIsabelle/HOL正式な仕様 |
| Kernkonzept gmbh | ドイツ | オペレーティングシステム | L4Re （ソース） |
| カスペルスキー | モスクワ、ロシア | セキュリティ/av | 合金、TLA、 Event-B （ソース）、 Ivory （ソース） |
| Machine Zone Inc. | ロシア | モバイルゲームソフトウェア、リアルタイムコンピューティング、クラウドベースのネットワーキング | TLA+ Twitter |
| マイクロソフト | 米国レドモンド | ソフトウェア開発 | TLA+ TLA+プルーフ、プログラマーの考え方、Azure Cosmos DBが提供する5つの一貫性レベルの高レベルTLA+仕様、 Microsoft's Static Driver Verifierデバイスドライバーの徹底的な静的分析Clousot的解釈、正式な方法、および分散型システムのための正式なシステムのための正式な方法のツールをチェック |
| mongodb | 米国ニューヨーク | ソフトウェア開発 | MongoDBレプリケーションシステムの単純化された部分のTLA+ TLA+仕様 |
| NASA | アメリカ合衆国 | 空間 | PVS NASA Langley Formals Methods Research Program。 JPF Java Pathfinder、堅牢なソフトウェアエンジニアリンググループ、 Model Checkingジェット推進研究所、 SPIN/Promelaのインスピレーションアプリケーション、 PVS （ソース） |
| 遊牧ラボ | パリ、フランス | ブロックチェーン | ソフトウェア検証に関するCoqページ |
| オラクル | 米国カリフォルニア州レッドウッドショアーズ | エンタープライズソフトウェア、クラウドコンピューティング、コンピューターハードウェア | ACL2 （ACL2を使用したJavaとJVMに関する定理を証明） |
| 特定のソフトウェア | NServiceBusのTLA+ TLA+仕様 | ||
| pingcap | TIDBのTLA+ TLA+ | ||
| プロバーテクノロジー | ヨーロッパ | 鉄道 | Model checking |
| rusbitech（陶芸） | モスクワ、ロシア | 見つけてください | Frama-C 、 Event-B （€€揮艦аниеиверикац遠物цполититикか番зопасноститопо措レ |
| ロックウェルコリンズ | 米国、アイオワ州シーダーラピッズ | 高保証システム | 航空宇宙産業の正式な方法：お金に従ってください |
| セロケル | タリン、エストニア | フィンテック、ブロックチェーン、IoT、機械学習、正式な検証 | Agda |
| 概要 | ？ | ？ | サイト |
| systerel | フランス | ソフトウェア、コンサルティング、サービス | S3シンクロン言語のモデルチェッカー、Bメソッド、イベントB/ロダン。採用。 |
| sifive | 米国、サンフランシスコベイエリア | ハードウェア | Coq LinkedIn |
| StateBox | オランダ、アムステルダム | ブロックチェーン | Idris （github） |
| スコイ | モスクワ、ロシア | 航空宇宙と防御 | ANSYS SCADE Suite （ソース - 光沢のための正式に検証されたコンパイラ） |
| タレス | Frama-C （共通基準認証のためのボトムアップ正式な検証アプローチ：Javacard仮想マシンへの申請） | ||
| Trustinsoft | 米国、カリフォルニア州サンフランシスコ | - | TrustInSoft Analyzerサイト |
| 信頼できるシステム | オーストラリア、シドニー | Isabelle/HOL 、 Coqサイト | |
| 2つの6つのテクノロジー | アメリカ合衆国 | 防衛研究 | Isabelle/HOL 、ハードウェア検証（例）、 Coq （例） |
| ジェットブレインの研究 | ロシア、聖ペテルブルク | - | Coq （ソース） |
| 回してください | モスクワ、ロシア | ？ | SPIN/Promelaゆズ名средстваверика牲愛протоколовビロギロシ |
| t-プラットフォーム | モスクワ、ロシア | - | Coq 、 SPIN/Promela 、 TLA+ 、 McErlang 、 mCRL2従業員cv |
| cern | ジェネーブ、スイス | CERNの大型ハドロンコリダーでのCMS実験のmCRL2コントロールソフトウェア | |
| yandex | ソフトウェア | TLA+クリックハウスレプリケーションアルゴリズム、ロックフリーメモリアロケーター | |
| zilliqa | シンガポール | ブロックチェーン | Coq SCILLA-COQプロジェクト |
| 波 | ブロックチェーン | ??? |
