verified-mbse

The Problem

VVRecord = { spec : Prop, verified : spec, validation : ValidationTrace spec }
 ───────────── ─────────────── ─────────────────────────────────
 requirement machine proof confidence trace (→ trusted)

Quick Start

1. Add to your project

-- lakefile.lean
require verifiedMbse from git
 "https://github.com/chantakan/verified-mbse.git"

2. Define components and a state machine

import VerifiedMBSE
open VerifiedMBSE.Core
open VerifiedMBSE.Behavior
open VerifiedMBSE.VV
-- A component with ports and an invariant
def PowerSupply : PartDef :=
 { baseType := { name := some "PowerSupply" }
 ports := [pwrOutPort]
 invariant := True }
-- State machine: invariant preservation is a *type-level contract*
-- (transitions that violate it simply won't compile)
def epsSM : StateMachine EPSMode Nat (fun _ v => v ≤ 1000) where
 initialState := .nominal
 transitions := [nominalToLowPower, lowPowerToFault, ...]

3. Bundle everything into one SubSystemSpec

def epsSpec : SubSystemSpec epsSM :=
 { structural := epsStructural -- System + WellFormed proof
 behavioral := epsBehavioral -- NonEmpty (Kripke-generalized)
 fdir := epsFDIR } -- Safety + Detection + Recovery proofs

4. Compose subsystems (N-way nested composition supported)

-- 2 subsystems
def epsAocsPK : ProductKripke epsSM aocsSM := ⟨⟩
def epsAocsSpec : SubSystemSpec epsAocsPK :=
 SubSystemSpec.compose epsSpec aocsSpec epsAocsPK
 epsSM_WellFormed.nonEmpty aocsSM_WellFormed.nonEmpty [] (by intros; contradiction)
-- 3 subsystems (nested) — enabled by B-8 ProductKripke generalization
def epsAocsTcsPK : ProductKripke epsAocsPK tcsSM := ⟨⟩
def epsAocsTcsSpec : SubSystemSpec epsAocsTcsPK :=
 SubSystemSpec.compose epsAocsSpec tcsSpec epsAocsTcsPK
 epsAocsSpec.behavioral.nonEmpty tcsSM_WellFormed.nonEmpty [] (by intros; contradiction)
-- N subsystems via variadic API (B-8d) — List.foldl-based composition
def sats : Option SubSystemPayload :=
 SubSystemPayload.composeMany
 [ SubSystemPayload.ofSpec epsSpec
 , SubSystemPayload.ofSpec aocsSpec
 , SubSystemPayload.ofSpec tcsSpec
 , SubSystemPayload.ofSpec ttcSpec ]

5. Build the V-Matrix and prove completeness

open VerifiedMBSE.Matrix
def satellite : VMatrix :=
 { columns := [epsColumn, aocsColumn, tcsColumn, ttcColumn] }
-- This theorem IS the verification: no gaps in the V-matrix.
theorem sat_complete : satellite.Complete ["EPS", "AOCS", "TCS", "TTC"] := by
 constructor
 · intro s hs; ... -- every subsystem has a column
 · intro col hcol; ... -- every column covers all layers

6. Generate human-readable outputs

open VerifiedMBSE.Output
#eval IO.println (satellite.toMarkdown "MySatellite")
#eval IO.println (satellite.toTerminal "MySatellite")

═══════════════════════════════════════════
 V-Matrix: MySatellite
 4 subsystems │ 25 records │ ALL TRUSTED
═══════════════════════════════════════════
 EPS [5] ████████████████████ 100%
 AOCS [6] ████████████████████ 100%
 TCS [8] ████████████████████ 100%
 TTC [6] ████████████████████ 100%
═══════════════════════════════════════════
 Completeness: ✓ All layers covered
═══════════════════════════════════════════

Module Structure

VerifiedMBSE/
├── Core/ # Domain-independent type-theoretic foundations
│ ├── KerML.lean # Element, KerMLType, Feature, Direction
│ ├── Port.lean # PortDef, Conjugation, compatible
│ ├── Specialization.lean # Specialization (preorder), FeatureTyping, Interpretation
│ ├── Component.lean # PartDef, PortRef, Connector, System, WellFormed
│ ├── Compose.lean # System.compose, compose_WellFormed
│ └── Interpretation.lean # PartInstance, ConnectorSemantic, categorical laws
│
├── Behavior/ # Behavioral models (Kripke-generalized LTL)
│ ├── StateMachine.lean # Transition, StateMachine, Reachable, inv_holds
│ ├── Temporal.lean # Always (□しろいしかく), Eventually (◇), Next, Until, Leads
│ ├── KripkeStructure.lean # KripkeStructure + ToKripke type class (B-1)
│ ├── StateMachineKripke.lean # StateMachine → KripkeStructure instance
│ ├── StateMachineLTL.lean # Dot-notation for sm.Always / sm.Eventually
│ ├── Product.lean # ProductStateMachine (abbrev of ProductKripke)
│ ├── ProductKripke.lean # ProductKripke (N-way nested, B-8)
│ ├── ProductTemporal.lean # Always_prod / Eventually_prod / Leads_prod lifting
│ └── FDIR.lean # FDIRSpec, StateMachineComponent
│
├── VV/ # Verification & Validation framework
│ ├── Layer.lean # Layer (8-level ECSS-E-ST-10C: mission→part)
│ ├── Evidence.lean # ValidationEvidence, isTrusted, ValidationTrace, VVRecord
│ ├── SubSystemSpec.lean # StructuralSpec, BehavioralSpec, FDIRBundle, SubSystemSpec
│ ├── VVBundle.lean # mkComponentRecord, SubSystemVVBundle, allRecords
│ ├── Power.lean # ModePowerSpec, PowerBudgetOK2
│ ├── Propagation.lean # LayerPropagation, depth-based supports
│ ├── Contract.lean # Contract, ContractedSystem, CouplingConstraint
│ ├── ProductFDIR.lean # FDIRBundle.compose, SubSystemSpec.compose (N-way)
│ └── VariadicCompose.lean # SubSystemPayload, composeMany (B-8d variadic)
│
├── Matrix/ # V-matrix construction
│ ├── VColumn.lean # VColumn, atLayer, Complete, fullyTrusted (struct-discrim)
│ ├── VMatrix.lean # VMatrix, SubSystemComplete, Complete
│ ├── Query.lean # column, cell, allRecords, summary
│ └── ModelBoundary.lean # ModelBoundary (vm : VMatrix) — dependently typed
│
├── Output/ # Human-readable output generation
│ ├── Render.lean # indent, typeName, layerToAbbr (8-layer)
│ ├── SysML.lean # → SysML v2 textual notation
│ ├── StateMachineSysML.lean # → SysML v2 state def
│ ├── Markdown.lean # → Markdown table
│ └── Terminal.lean # → Terminal summary with confidence bars
│
└── Equivalence/ # HoTT-inspired equivalence (advanced)
 ├── ComponentEquiv.lean # PortEquiv, ComponentEquiv, Substitutable
 ├── Refinement.lean # DesignEquiv, RequirementRefinement
 ├── Abstraction.lean # AbstractionLevel, DesignParameter
 └── Univalence.lean # DesignSpace (quotient), ua/ua_inv, Transport, Fiber
Examples/Spacecraft/ # Full satellite case study + acceptance tests
├── EPS.lean # Electric Power Subsystem (+ EPSTypeTag F8 pattern)
├── AOCS.lean # Attitude & Orbit Control
├── TCS.lean # Thermal Control (mode-dependent invariants)
├── TTC.lean # Telemetry, Tracking & Command
├── Satellite.lean # V-Matrix + completeness + ModelBoundary
├── Integration.lean # 2-way and 3-way nested composition sanity tests
├── F1F2Tests.lean # Evidence parameterization + mixed-evidence tests
├── F3F5F6Tests.lean # Specialization preorder, Layer 8-level, ModelBoundary type-binding
├── F8Tests.lean # Interpretation pattern (EPSTypeTag + exhaustive dispatch)
└── VariadicComposeTests.lean # B-8d payload / compose / composeMany sanity tests

Key Types at a Glance

Design Principles

Documentation

Requirements

Statistics

License