VerifiedMBSE

A Lean 4 framework that gives SysML v2 / KerML design models a dependent type-theoretic semantics and guarantees V&V matrix completeness by type checking.

Modules

• Core — KerML elements, ports, specialization, components, connectors, system composition, categorical interpretation.
• Behavior — Unified Kripke-based LTL framework via ToKripke type class. KripkeStructure State Data は LTL 演算子 (Always / Eventually / Leads) の共通意味論基盤で、ToKripke 型クラスを通して StateMachine / ProductStateMachine / 連続時間系などが同一 API を共有する。Next / Until は 遷移構造に依存するため StateMachineLTL に分離。FDIR, Product (積状態機械の到達可能性), ProductKripke (積の ToKripke instance), ProductTemporal (Always_prod 等の後方互換エイリアス + 持ち上げ補題) を含む。
• VV — StructuralSpec / BehavioralSpec / FDIRBundle / SubSystemSpec による統合仕様、evidence 付き ValidationTrace、ModelBoundary。 B-6/B-7 により FDIRBundle / BehavioralSpec / SubSystemSpec は ToKripke α S D ベースに一般化され、SubSystemSpec sm / SubSystemSpec psm が同一構造体型で扱える。並列合成は SubSystemSpec.compose で、 N 機はそのネストで実現する。
• Matrix — VColumn / VMatrix による V&V マトリクス、完全性定理、 VMatrix に依存型紐付けされた ModelBoundary。
• Output — SysML v2 テキスト記法、Markdown テーブル、端末表示。
• Equivalence — HoTT 風等価性: ComponentEquiv / DesignSpace (quotient) / ua / transport / RequirementRefinement / AbstractionLevel。

Roadmap (F4.5: Kripke Unification)

B-1 (KripkeStructure + ToKripke 導入)・B-4 (ProductStateMachine 統合)・ B-6 (ProductFDIRBundle → FDIRBundle 合流)・B-7 (SubSystemSpec の Kripke 一般化 + 2機合成) を完了。以降 B-8 (型クラスベースの可変長 N 機合成 API)、連続時間系への拡張 (F10) と段階的に進める。