kaniで数学的に証明するRust標準ライブラリの安全性本記事はエクサウィザーズの Advent Calendar 15日目の記事です。 本記事の目標 先端技術開発グループ（WAND）の佐藤碧です。2025年12月にAWSで開催されたAWS re:Inventに参加してきました。 このChalk talkの一つに「Verifying the safety of the Rust standard library」というものがあり、ここで紹介されていたkaniというAmazonが作成しているOSSがとても面白いものでした。kaniがどのようなOSSかを解説し、使い方の一例を紹介します。 Rust standard library Rustのcoreとstdクレートには27,000以上の関数が含まれています。このうち、unsafeな関数は7,000以上あり、unsafeなコードを安全にラップしたものは2,300以上あります。 標準ライブラリのバグは
