マルティン・アバディ（Martín Abadi）
セキュリティプロトコルを「証明できるもの」に変え、同じ厳密さを機械学習にも持ち込んだ、アルゼンチン出身の計算機科学者。
BAN 論理（1989年、マイケル・バロウズ、ロジャー・ニーダムとの共著）は、認証プロトコルの参加者が何を信じてよいかを論じる、初の実用的な形式手法だった。1997年にはアンドルー・ゴードンとスパイ計算（spi calculus）を開発し、ニーダムとはプロトコル設計の賢明な作法をまとめた。形式手法が見逃すバグを今も拾ってくれる指針である。
2005年にはマイクロソフトリサーチの同僚らと制御フロー完全性（CFI）を提案し、現在ではコンパイラや CPU にも組み込まれている。Google では TensorFlow の共著者となり、2016年には差分プライバシー付きの深層学習手法も発表した。これほど分野を渡り歩きながら、「システムは実際に何を保証するのか」という問いから一度も離れなかった人は珍しい。