展示計畫：基於 Google Zanzibar 架構的 Lean4 Datalog DSL (ZIL)
為何重要
此工具重新定義了軟體專案知識管理的方式，將靜態程式碼轉化為結構化的圖形資料庫，使複雜系統間的依賴關係成為可推算的資料。這對於依賴嚴謹型別與形式化驗證的專案（如 Lean 或金融工程）帶來了自動化檔案與合約檢核的潛力，降低維護複雜度與人為疏失的風險，是資訊流追蹤技術的一個有趣實驗。
- 核心架構：ZIL 是一種建構在 Lean 4 環境中的小型關係式語言（DSL），靈感來自 Google Zanzibar 系統，旨在描述物件、相關性與推導規則。
- 關係模型：採用元組模型定義宣告、需求、測試與工具之間的連結，並支援透過 Horn 規則（常見於 Datalog）推論出新增的關係。
- 應用場景：可解答跨模組的全域查詢，例如需求覆蓋率分析、變更影響範圍追蹤，以及開發者、CI 系統與 AI 助手共享的專案圖譜維護。