Lean 4で「正しさ」を証明してから書く——AIエージェントと作った検証済みコンパイラ基盤で macro_peg の意味論まで証明した話

Lean 4で型検査器、インタプリタ、コンパイラを「正しさ」を証明した上で実装し、AIエージェントと協力してScala 3への自動変換基盤を構築。PEG拡張形式macro_pegの意味論も証明。

• Lean 4を用いて、PEGベースのコンパイラ基盤の正しさを形式的に証明した事例を紹介しています。
• AIエージェントと共同で、型検査器、インタプリタ、コンパイラ等を実装し、その意味論まで証明しました。
• 証明済みのLean 4コードをScala 3へ変換する抽出器「Lens」を開発し、バグ混入リスクを低減しています。
• macro_peg の3つの評価戦略の意味論を形式化し、基盤の信頼性をさらに高めたことを報告しています。