2026年7月28日 LLMはコードの正しさを証明できないが、証明のための定型作業は書ける クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。 cleanroom-correctnessllmformal-proofsautomation
2026年7月27日 Cleanroom は 1KLOC あたり 0.1 defect を達成する。フル導入しなくてもそこに到達できる。 Cleanroom software engineering は defect rate を 100 倍に削減するが、フル導入には分離した test team と formal proof が必要。ここでは、overhead なしにその大半の benefit を得られる pragmatism なサブセットを紹介する。 cleanroom-correctnessprocessefficiencypragmatism
2026年7月26日 IBMのZero-Defect ProcessはKLOCあたり0.1 Bugを達成した。それでも業界は見捨てた。 IBMのCleanroom engineeringは業界平均より100倍優れたdefect rateを達成し、その後忘れ去られた。消えた理由は、それが機能したかどうかとは無関係だった。 cleanroom-correctnesszero-defectssoftware-historyprocess
2026年7月25日 本当に1万行を零欠陥で検証した人がいるのか？IBMはやったし、その方法論は結果より奇妙だ。 Cleanroom software engineeringは、デバッグではなくmathematical verificationによって零欠陥のインクリメントを約束した。我々はIBMの実プロジェクトデータを見て、その主張が成り立ったかを確認する。 cleanroom-correctnesszero-defectsverificationcase-study
2026年7月24日 あなたのモジュールには3層ある。書いたのは1層だけだろう。 Box Structureは、モジュールが何をするか、何を記憶するか、どう動作するかを、3つの独立した検証可能な層として定義することを強制する。Cleanroomがどうやってデバッグを排除するか、ここで解説する。 cleanroom-correctnessbox-structurearchitecturespecification
2026年7月23日 IBM は開発者に自身のコード実行を禁止し、0.1 defects/KLOC のソフトウェアを出荷した IBM の Cleanroom エンジニアリング・プロセスは、バグを発見するのではなく未然に防ぐことで、業界平均より 100 倍優れた defect 率を達成した。それがどう機能したか、なぜほとんど誰も使わないのか、そして今日あなたが取り入れられるものとは。 cleanroom-correctnessibmzero-defectssoftware-quality
