2026年7月9日 AutoVerusは40時間の証明執筆を3回のLLM呼び出しに変える。秘訣は諦めるタイミングを知ることだ。 AutoVerusはLLMエージェントのネットワークを用いてRustコードのVerus正しさ証明を生成し、SMTソルバーのフィードバックによって駆動される生成・修復・ dischargeループにより、90%以上の証明義務を自動化する。 model-checkingautoverusrustverification
2026年7月8日 LLMはRustコードを生成できる。形式的証明は全く別の問題だ。 大規模言語モデルは驚くほど質の高いRustコードを書くが、形式的証明を求めると、不変条件を幻覚で見つけ、どの検証器も受け付けない構文をでっち上げる。それらが実際に正しい部分、壊れる部分、それでも使う方法を解説する。 model-checkingllmrustformal-proofs
2026年7月5日 一行の証明も書かずに Rust コードの正しさを証明できるが、状態空間が代償となる Kani のようなモデル検査ツールを使えば、形式的証明の代わりに表明で Rust の性質を検証できる。問題は、ループの境界が小さくないときに何が起きるかだ。 model-checkingrustverificationformal-methods
2026年6月26日 依存ライブラリがディスク上の任意のファイルを読める。cap-std は許可を求めさせる Rust の標準ライブラリはあらゆる依存ライブラリに対して、暗黙的なファイルシステム権限を付与する。cap-std はそれを能力ベースの API に置き換え、コードがパスを開く前にそのアクセス権を証明することを強制する。 capability-based-securityrustcap-stdsandboxing
2026年6月22日 throw するのをやめて、エラーを返すべきか 例外を投げると、型システムから失敗の経路が見えなくなる。明示的なエラー返却がコードをより正直にする理由と、それを苦痛なく導入する方法。 type-level-correctnesserror-handlingtypescriptrust
2026年6月21日 Rustのnewtypeで、誤った状態をコンパイル時に無償で表現不能にする 1フィールドのラッパー構造体が、1バイトのオーバーヘッドも増やさずに単位混在バグや型の混同を防ぐ。 type-level-correctnessrustnewtypeszero-cost-abstractions
2026年5月28日 RustでMutation Testingは機能する——ただしコンパイル時間が悲鳴を上げる cargo-mutantsは、コードを検証したふりをしているテストを見つけ出す。Rustでのmutation testingの仕組み、何が捉えられるのか、そしてコンパイル時間のコストに見合う価値があるかを解説する。 deep-divesmutation-testingrustcargo-mutantstest-quality
2026年5月23日 Rustのプロパティベーステストが単体テストでは見逃すバグを見つける 例ベースのテストは思いついた入力だけをカバーする。プロパティベースのテストはランダムデータを生成し、不変条件を検証し、失敗を最小の反例まで縮小する。 deep-divesrustproperty-based-testingquickcheckproptest
2026年5月21日 Rustのランタイムcontractsはリリースビルドで無料にできるが、コンパイラは勝手にやってくれない Rustはdebug assertionsを自動で除去するが、本物のdesign-by-contractにはdebug_assert!以上のものが必要だ。リリースバイナリーから完全に消えるゼロコストのランタイムcontractsを作る方法を紹介する。 deep-divesrustruntime-contractsperformance
