Lean 4をRTL開発の中核にする — Sparkle におけるJIT、検証、Reverse Synthesis(逆合成)

橋本順之@junjihashimoto32026年7月11日Track A50 分

Lean 4をRTL開発の中核に据えるSparkleを紹介。JIT実行、証明駆動の時間跳躍、逆合成による高速化など、証明を実行最適化に使う設計が分かる。

発表概要の全文は fortee の発表ページ で読めます。