Amazon

ツールはよくわからない。独自？

Amazon S3の軽量形式手法 - masateruk’s blog

DeNA

Spin

3．形式手法を応用した、仕様段階でのバグの検出　a．形式手法（Spin／Promela等）を利用し、仕様の形式記述言語を表現し、仕様バグを早期に発見する　b．形式記述言語支援ツールの開発

プログラマー | 株式会社ディー･エヌ･エーの求人詳細 | ゲーム業界の転職・求人情報ならファミキャリ！ - ファミ通.com

Alloy

DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました（録画・スライドあり） - DeNA Testing Blog

なかなかいいな。就職するには、会社の業績も気になるところ。業績悪化で、型式手法の適用中止になったら、詰むよね。まあ、日本で型式手法が必須な産業はあるのか知りません。適用したらもとが取れる分野はあると信じたい。

レピダム

Coq

Heartbleedが公開されたときに、どのようにして次のバグを防ぐかが話題になっていました。ユニットテストを使うとか、各種アナライザーツールで検査するとか、フォークして綺麗に書き直してみるとか、APIも悪いとか、mallocを自作してはいけないとか、C言語はよくないから他の言語を使うべきとかいろいろありました。

他の言語の候補としてはATSが人気のようでしたが、自分の使い慣れているCoqでTLS/SSLを実装するとどうなるか考えていました。プロトコルの安全性の証明などは大変ですし、実装の安全性にはたいして寄与しないので、見ただけで正しい実装をしているとすぐに確認できる程度のものを作ることを考えていました。

CCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介｜レピダム