Model Boundary: Explicit Declaration of What Is Not Verified

Formal verification only guarantees properties on the inside of a model. This module treats the outside of the model as a first-class object so that "the V&V matrix is green" is not conflated with "the real system is safe".

A ModelBoundary records:

• properties verified formally,
• properties supported by test or analysis rather than proof, and
• residual risks deliberately left out of the model, each annotated with a rationale and a mitigation.

The intent is epistemic honesty, not bookkeeping. When the system changes, the boundary description should be revisited.

Dependency on VMatrix

ModelBoundary is parameterized by the VMatrix it describes: ModelBoundary (vm : VMatrix). Accidentally reusing a boundary description for a different system therefore produces a type error. The verifiedCount field is not stored but derived as a function of vm.totalRecords, so it cannot drift out of sync with the matrix.

Because of the VMatrix dependency, this file lives in the Matrix namespace rather than VV.

inductive VerifiedMBSE.Matrix.RiskCategory : Type

Category of an unmodeled risk.

• physical : RiskCategory

  Physical phenomena outside the formal model (single-event upsets from cosmic rays, micrometeoroid impact, material fatigue, ...).

• environmental : RiskCategory

  Environmental factors (solar activity, thermal extremes, radiation).

• human : RiskCategory

  Human factors (operator error, procedure misuse, inadequate training).

• software : RiskCategory

  Software risks outside the verification boundary (COTS, firmware, OS).

• hardware : RiskCategory

  Hardware risks (manufacturing defects, aging, part substitution).

• organizational : RiskCategory

  Organizational and process risks (change management, supply chain).

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprRiskCategory : Repr RiskCategory

Equations

• VerifiedMBSE.Matrix.instReprRiskCategory = { reprPrec := VerifiedMBSE.Matrix.instReprRiskCategory.repr }

def VerifiedMBSE.Matrix.instReprRiskCategory.repr : RiskCategory → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instBEqRiskCategory : BEq RiskCategory

Equations

• VerifiedMBSE.Matrix.instBEqRiskCategory = { beq := VerifiedMBSE.Matrix.instBEqRiskCategory.beq }

def VerifiedMBSE.Matrix.instBEqRiskCategory.beq : RiskCategory → RiskCategory → Bool

Equations

• VerifiedMBSE.Matrix.instBEqRiskCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instDecidableEqRiskCategory : DecidableEq RiskCategory

Equations

• VerifiedMBSE.Matrix.instDecidableEqRiskCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.Matrix.RiskCategory.toString : RiskCategory → String

Human-readable category name.

Equations

• VerifiedMBSE.Matrix.RiskCategory.physical.toString = "Physical"
• VerifiedMBSE.Matrix.RiskCategory.environmental.toString = "Environmental"
• VerifiedMBSE.Matrix.RiskCategory.human.toString = "Human"
• VerifiedMBSE.Matrix.RiskCategory.software.toString = "Software"
• VerifiedMBSE.Matrix.RiskCategory.hardware.toString = "Hardware"
• VerifiedMBSE.Matrix.RiskCategory.organizational.toString = "Organizational"

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instToStringRiskCategory : ToString RiskCategory

Equations

• VerifiedMBSE.Matrix.instToStringRiskCategory = { toString := VerifiedMBSE.Matrix.RiskCategory.toString }

inductive VerifiedMBSE.Matrix.EvidenceKind : Type

Strength of the evidence supporting a property. Distinguishes proof from test and analysis so that ModelBoundary does not hide the difference.

• verified : EvidenceKind

  Formal proof in Lean.

• tested : EvidenceKind

  Supported by a test campaign (unit test, HIL, qualification).

• analyzed : EvidenceKind

  Supported by an analysis method (FMEA, FTA, Monte Carlo).

def VerifiedMBSE.Matrix.instReprEvidenceKind.repr : EvidenceKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprEvidenceKind : Repr EvidenceKind

Equations

• VerifiedMBSE.Matrix.instReprEvidenceKind = { reprPrec := VerifiedMBSE.Matrix.instReprEvidenceKind.repr }

def VerifiedMBSE.Matrix.instBEqEvidenceKind.beq : EvidenceKind → EvidenceKind → Bool

Equations

• VerifiedMBSE.Matrix.instBEqEvidenceKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instBEqEvidenceKind : BEq EvidenceKind

Equations

• VerifiedMBSE.Matrix.instBEqEvidenceKind = { beq := VerifiedMBSE.Matrix.instBEqEvidenceKind.beq }

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instDecidableEqEvidenceKind : DecidableEq EvidenceKind

Equations

• VerifiedMBSE.Matrix.instDecidableEqEvidenceKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.Matrix.EvidenceKind.toString : EvidenceKind → String

Human-readable evidence-kind name.

Equations

• VerifiedMBSE.Matrix.EvidenceKind.verified.toString = "Verified"
• VerifiedMBSE.Matrix.EvidenceKind.tested.toString = "Tested"
• VerifiedMBSE.Matrix.EvidenceKind.analyzed.toString = "Analyzed"

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instToStringEvidenceKind : ToString EvidenceKind

Equations

• VerifiedMBSE.Matrix.instToStringEvidenceKind = { toString := VerifiedMBSE.Matrix.EvidenceKind.toString }

structure VerifiedMBSE.Matrix.UnmodeledRisk : Type

A risk the formal model does not cover. Requires an explicit rationale and mitigation so the engineer is forced to name and justify the gap.

• description : String

  Short description of the risk.

• category : RiskCategory

  Category of the risk.

• rationale : String

  Rationale for leaving this risk out of the formal model.

• mitigation : String

  Non-formal mitigation (process, test, redundancy, operational constraint).

def VerifiedMBSE.Matrix.instReprUnmodeledRisk.repr : UnmodeledRisk → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprUnmodeledRisk : Repr UnmodeledRisk

Equations

• VerifiedMBSE.Matrix.instReprUnmodeledRisk = { reprPrec := VerifiedMBSE.Matrix.instReprUnmodeledRisk.repr }

structure VerifiedMBSE.Matrix.NonFormalProperty : Type

A property supported by test or analysis but not proved formally.

• description : String

  Description of the property.

• kind : EvidenceKind

  Kind of non-formal evidence (.tested or .analyzed).

• source : String

  Reference to the supporting source (report ID, test campaign name, ...).

def VerifiedMBSE.Matrix.instReprNonFormalProperty.repr : NonFormalProperty → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprNonFormalProperty : Repr NonFormalProperty

Equations

• VerifiedMBSE.Matrix.instReprNonFormalProperty = { reprPrec := VerifiedMBSE.Matrix.instReprNonFormalProperty.repr }

structure VerifiedMBSE.Matrix.ModelBoundary (vm : VMatrix) : Type

Composite view of what the model covers together with the risks outside it.

Parameterizing by the target VMatrix ties the boundary to a specific matrix: accidentally reusing a boundary description for a different system produces a type error. verifiedCount is derived from vm.totalRecords as a function rather than stored, so it cannot drift out of sync.

• systemName : String

  Identifier of this boundary (typically the system name).

• nonFormal : List NonFormalProperty

  Properties supported by test or analysis but not proved.

• unmodeled : List UnmodeledRisk

  Risks deliberately left out of the formal model.

@[implicit_reducible]

instance VerifiedMBSE.Matrix.instReprModelBoundary {vm✝ : VMatrix} : Repr (ModelBoundary vm✝)

Equations

• VerifiedMBSE.Matrix.instReprModelBoundary = { reprPrec := VerifiedMBSE.Matrix.instReprModelBoundary.repr }

def VerifiedMBSE.Matrix.instReprModelBoundary.repr {vm✝ : VMatrix} : ModelBoundary vm✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Matrix.ModelBoundary.verifiedCount {vm : VMatrix} : ModelBoundary vm → Nat

Number of formally verified properties, derived from the total record count of the target VMatrix.

Equations

• x✝.verifiedCount = vm.totalRecords

def VerifiedMBSE.Matrix.ModelBoundary.unmodeledCount {vm : VMatrix} (mb : ModelBoundary vm) : Nat

Number of unmodeled risks.

Equations

• mb.unmodeledCount = mb.unmodeled.length

def VerifiedMBSE.Matrix.ModelBoundary.nonFormalCount {vm : VMatrix} (mb : ModelBoundary vm) : Nat

Number of non-formal properties.

Equations

• mb.nonFormalCount = mb.nonFormal.length

def VerifiedMBSE.Matrix.ModelBoundary.totalItems {vm : VMatrix} (mb : ModelBoundary vm) : Nat

Total number of tracked items (verified + non-formal + unmodeled).

Equations

• mb.totalItems = mb.verifiedCount + mb.nonFormalCount + mb.unmodeledCount

def VerifiedMBSE.Matrix.ModelBoundary.risksInCategory {vm : VMatrix} (mb : ModelBoundary vm) (cat : RiskCategory) : List UnmodeledRisk

Filter unmodeled risks by category.

Equations

• mb.risksInCategory cat = List.filter (fun (r : VerifiedMBSE.Matrix.UnmodeledRisk) => r.category == cat) mb.unmodeled

def VerifiedMBSE.Matrix.ModelBoundary.summary {vm : VMatrix} (mb : ModelBoundary vm) : String

Render a ModelBoundary as a human-readable summary string.

Equations

• One or more equations did not get rendered due to their size.