2026年7月28日 LLMはコードの正しさを証明できないが、証明のための定型作業は書ける クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。 cleanroom-correctnessllmformal-proofsautomation
2026年7月22日 CI があなたなしで tangle できない限り、あなたのリテラート・プログラムは壊れている Literate programming は単一事実情報源を約束するが、手動の weave と tangle のステップが CI/CD パイプラインを破壊する。Markdown ファイルを正規のものに保つため、抽出とドキュメント生成を自動化する方法を紹介する。 literate-programmingci-cdweave-tangleautomation
