CONSTANTS
    D1 = d1
    S1 = s1
    S2 = s2
    R1 = r1
    R2 = r2
    R3 = r3
    ExactCmd = exactCmd
    PromptCmd = promptCmd
    ShellCmd = shellCmd
    EditedCmd = editedCmd
    Identities <- IdentitiesFixture
    SessionAnchors <- SessionAnchorsFixture
    Domains <- DomainsFixture
    Sessions <- SessionsFixture
    Requests <- RequestsFixture
    Commands <- CommandsFixture
    NoSession = NoSession
    NoRequest = NoRequest
    NoCommand = NoCommand
    NoApproval = NoApproval
    SessionDomain <- SessionDomainFixture
    SessionFingerprint <- SessionFingerprintFixture
    DomainFingerprint <- DomainFingerprintFixture
    DomainCoordinatorIdentity <- DomainCoordinatorIdentityFixture
    DomainSidecarIdentity <- DomainSidecarIdentityFixture
    DomainSandboxIdentity <- DomainSandboxIdentityFixture
    SessionCliIdentity <- SessionCliIdentityFixture
    SessionAnchorIdentity <- SessionAnchorIdentityFixture
    CoordinatorCertificateValid <- CoordinatorCertificateValidFixture
    SidecarCertificateValid <- SidecarCertificateValidFixture
    SandboxCertificateValid <- SandboxCertificateValidFixture
    CliCertificateValid <- CliCertificateValidFixture
    ConfigSafe <- ConfigSafeFixture
    SandboxIsolationSafe <- SandboxIsolationSafeFixture
    RequestSession <- RequestSessionFixture
    RequestCommand <- RequestCommandFixture
    RequestSandboxIdentity <- RequestSandboxIdentityFixture
    RequestCliIdentity <- RequestCliIdentityFixture
    RequestSessionAnchor <- RequestSessionAnchorFixture
    RequestCredentialValid <- RequestCredentialValidFixture
    RequestSignatureValid <- RequestSignatureValidFixture
    ApprovalCliIdentity <- ApprovalCliIdentityFixture
    ApprovalSessionAnchor <- ApprovalSessionAnchorFixture
    ApprovalSignatureValid <- ApprovalSignatureValidFixture
    ApprovalCommand <- ApprovalCommandFixture
    AutoRuleMatches <- AutoRuleMatchesFixture
    CommandRequiresShell <- CommandRequiresShellFixture
    CommandContentSafe <- CommandContentSafeFixture
    TerminalEventPlan <- TerminalEventPlanFixture
    TerminalAuthorityPlan <- TerminalAuthorityPlanFixture
    TerminalAdministrativeAuthorityValid <-
        TerminalAdministrativeAuthorityValidFixture
    TerminalRoutingFault = "Correct"

SPECIFICATION SafetySpec
CHECK_DEADLOCK FALSE

INVARIANTS
    TypeOK
    SessionTerminalPhysicalConsistency
    ConfigurationConfinement
    SandboxNamespaceIsolation
    OrderedNetworkStartup
    PublishedDomainsReady
    DomainLockLifetime
    RuntimeCausalEdgeArmedBeforeSandbox
    RuntimeCausalEdgeOwnerPresent
    SandboxRunningImpliesCoordinatorPresent
    PublishedRuntimeAuthorityPresent
    SupervisorLeaseConsistency
    RuntimeResourceOwnership
    CoordinatorPhysicalConsistency
    HostCoordinatorRequiresDomainOwnership
    NoVanishPresentRuntime
    OrderedLeaseTeardown
    DomainGenerationBounds
    DurableIntentBeforeSandboxReady
    DurableDecisionPublicationConsistent
    PathMismatchNotAdopted
    ExclusiveBootstrapOwnership
    TeardownNotJoinable
    RegisteredSessionsConnected
    AttachedSessionsValid
    AuthenticatedRequestsOnly
    RuntimeRoleIdentitySeparation
    RegisteredSessionIdentityUniqueness
    LiveRequestIdentityAuthorized
    DeveloperApprovalAuthenticated
    HostExecutionAuthorized
    AutoApprovalNoShell
    TerminalIsolation
    TerminalInteractionAuthoritySeparated
    LocalTerminationAvailableWhileTransportBlocked
    NoOrphanHostProcess
    StateAnchorOwnership
    FailedDomainIsolation
    OrderedFailureRecovery
    ResultDeliveryStateConsistent
    MultiRoleDurableIntent
    NetworkReadinessBoundToSandbox
    GenerationScopedIdentitiesDistinct
    HelperUnderSupervisor
    PreparedLowerLeaseBeforeMount
    NetworkReadyBeforePublish