AutoVerusは40時間の証明執筆を3回のLLM呼び出しに変える。秘訣は諦めるタイミングを知ることだ。
AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。
形式的検証で最も難しいのは、検証器そのものではない。証明を書くことだ。 熟練のRustエンジニアにMicrosoft…
model-checking
6 posts
LLMはRustコードを生成できる。形式的証明は全く別の問題だ。
大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。
LLMはコンパイルできても通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。…
race conditionを待つのは最悪のテスト戦略だ
model checkingが、concurrency bugを発見するためにアプリを数日間実行することをどう凌駕するか、そして自分のコードにどう応用するか。
productionでrace conditionが出るのを待つのは、テストじゃない。勤勉のフリをした希望だ。 アプリを何週間も走らせ、metrics dashboardを見張っていても、2つのrequestがまさに同じcache eviction windowに突入したときだけ発火するconcurrency…
時相論理を学ばずにコードのモデル検査ができる
Kaniのような境界付きモデル検査器やAlloyのような関係モデルファインダーは、通常のアサーションと制約で性質を検証できる。活性の証明を諦める代わりに、学習曲線は週ではなく時間単位で測られる。
モデル検査器を使うために線形時相論理を学ぶ必要はない。Kani、CBMC、Alloyのようなツールは、通常のアサーションと関係制約で性質を検証できる。活性を証明する能力と引き換えに、学習曲線は週ではなく時間単位で測られ、ほとんどのソフトウェアのバグに対してそれは見合う交換だ。…
一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる
Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。
一行の証明も書かずに Rust コードの正しさを証明できる。その仕事をするのがモデル検査器であり、現時点で Rust に最も実用的なものは AWS が開発した Kani だ。通常の Rust の表明を書けばよい。Kani…
分散プロトコルは単体テストできないが、モデル検証はできる
分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。
分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。…