Microsoft、SymCrypt の Rust 暗号実装を Lean で形式検証──SHA-3 と ML-KEM を公開
Rust のメモリ安全性と Lean による数学的証明を組み合わせ、Windows や Azure で稼働する暗号ライブラリの正当性を担保する新手法を確立した。
素数が作る3次元迷路の到達性を解明──定数cで57倍変化しFCC格子の臨界値と整合
座標のノルムが素数であるかという数論的制約が、物理的なパーコレーション閾値と一致することを証明し、事前登録検証で実測値との誤差0.02%を達成した。