model-checkingautoverusrustverification AutoVerusは40時間の証明執筆を3回のLLM呼び出しに変える。秘訣は諦めるタイミングを知ることだ。 AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。 形式的検証で最も難しいのは、検証器そのものではない。証明を書くことだ。 熟練のRustエンジニアにMicrosoft… 2026年7月9日