×

Compliance

Challenges

  • Controls span policies, systems, owners, evidence sources, and review periods.
  • Manual evidence collection is repetitive and difficult to reproduce.
  • Exceptions can obscure whether a control is absent, failed, or not applicable.
  • Audit conclusions must remain linked to current rules and supporting records.

Problems We Solve

  • Control Mapping Connect obligations, controls, owners, and evidence sources.
  • Evidence Checking Evaluate whether required records are present and current.
  • Exception Analysis Classify gaps and route them through explicit review paths.
  • Consistency Validation Check alignment between policy, control, and implementation.
  • Audit Preparation Assemble traceable placeholder evidence and decision records.

Domain portfolio

Application patterns

Compare two formal-assurance approaches, then explore the domain workflows as interactive state machines.

The Compliance domain links obligations, policies, controls, owners, evidence, exceptions, and audits. Beyond collecting records, teams must preserve applicability, control purpose, operating evidence, and authority to resolve gaps. These examples use FF Scribe to confirm tightly scoped propositions without making current-rule or jurisdictional claims. Interpretation, risk acceptance, control ownership, and assurance conclusions remain with accountable professionals.
01 Obligation-to-control mapping and design assessment Explore pattern

System/use case

A compliance requirements platform formalizes mapping assertions between a governed obligation, internal policy statement, control objective, control activity, accountable owner, and evidence source. It supports new-requirement intake, control rationalization, and review of whether a proposed control description addresses the intended obligation boundary.

Operational setting

Compliance advisory teams maintain approved obligations and applicability decisions. Policy owners maintain internal standards; first-line owners document controls; second-line compliance reviews mappings and challenges gaps. Changes capture effective periods, business and product scope, rationale, and sign-off. Internal audit can use the lineage without inheriting management’s conclusion.

Decision/claim boundary

The proposition may state a mapping or review condition, such as when an applicable obligation requires an approved control and owner. It cannot decide legal applicability, interpret an obligation, establish that a control is well designed, or show that it operates effectively. The designated compliance authority owns interpretation and mapping approval; the control owner remains accountable for design and operation.

Candidate checked statements

These are illustrative controlled-English propositions for a possible setup, not capabilities or rules already implemented:

  • For every applicable obligation, if no approved control mapping is recorded, then the obligation requires compliance review.
  • For every control mapping, if the obligation scope changes, then the mapping requires reassessment.
  • For every control, if an accountable owner and an approved evidence source are recorded, then the control is eligible for design review.

Example architecture

A repository separates versioned source material from approved internal interpretations. A graph links obligation versions, applicability decisions, policies, controls, systems, owners, risks, and evidence. Workflow enforces roles and dates; impact analysis exposes downstream mappings. During rule review, FF Scribe output is stored with setup, source and mapping versions, compiler result, readback ID, and practitioner response. Only authorized reviewers approve mappings; the model cannot modify obligations or interpretations.

Where verified readback fits

An analyst describes the intended mapping or reassessment condition in natural language. The model proposes one proposition within a deliberately small setup vocabulary. Agda accepts or rejects it on syntax and type grounds. If the separate partial readback stage supports the checked structure, it emits the finite audited family with semantic-rule provenance; otherwise it fails visibly without partial prose. The analyst accepts a successful reading or provides feedback. Acceptance confirms the statement’s intended meaning; it does not make the interpretation authoritative or prove that the control addresses the obligation.

Potential benefits

  • Makes obligation, applicability, control, owner, and evidence relationships explicit for multidisciplinary review.
  • Preserves reproducible meaning across requirement-version and policy changes.
  • Improves impact analysis by attaching confirmed propositions to governed graph relationships.
  • Reduces semantic drift between compliance narratives, control libraries, engineering requirements, and audit walkthroughs.

Limits/adoption considerations

A type-correct proposition is structurally valid in the selected setup, not legally correct, factually true, or evidence of control design effectiveness. FF Scribe checks the proposition type rather than completing a proof that a mapping exists or is adequate. Practitioner confirmation establishes user intent, not approval authority. Source licensing, version provenance, privilege, interpretive governance, access control, and independent challenge remain essential. Complex exceptions, negation, disjunction, and temporal applicability require explicit supported formal structures; opaque labels should not conceal unmodeled reasoning.
02 Continuous control evidence and exception triage Explore pattern

System/use case

A continuous compliance monitoring service formalizes the conditions under which evidence is current, a control observation is reviewable, and an exception is routed as missing, failed, stale, contradictory, or not applicable. It targets high-volume controls whose artifacts originate in identity, change, configuration, transaction, or ticketing systems.

Operational setting

Connectors collect integrity-protected evidence packages from systems of record on defined schedules. A monitoring engine evaluates completeness and freshness, records population and period, and creates exceptions. First-line owners investigate; second-line compliance reviews material or recurring deviations; internal audit can inspect provenance without adopting the monitoring conclusion.

Decision/claim boundary

The checked statement defines evidence-handling logic or an escalation boundary. It does not establish that evidence is authentic, that the tested population is complete, that the control operated as described, or that a monitoring algorithm is valid. The control owner attests to operation; the compliance oversight function approves exception taxonomy and escalation policy.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every control execution and review period, if required evidence is absent, then the execution is classified for missing-evidence review.
  • For every evidence record, if its observation period differs from the control period, then the record does not satisfy the current evidence request.
  • For every recurring exception, if the approved recurrence threshold is met, then the exception requires compliance escalation.

Example architecture

Source-specific collectors send metadata and artifacts to a write-once evidence store. A schema registry identifies control, population, period, system, collector, and integrity fields. The monitoring service evaluates configured checks and sends reason-coded cases to a workflow platform. Dashboards consume the case state, not raw unreviewed conclusions. FF Scribe supports authoring and review of classification and routing propositions, with accepted readings bound to rule versions and test fixtures. Trust is layered: collectors establish provenance, monitoring computes observations, practitioners adjudicate meaning and disposition, and independent assurance evaluates the overall design.

Where verified readback fits

A control specialist describes a classification or escalation condition. The model maps that request to a setup-scoped proposition, and Agda verifies that the candidate is a valid type in the registered vocabulary. For supported structure, the partial readback stage presents audited canonical, compact, evidence-oriented, or structured readings; unsupported translation fails visibly. The specialist explicitly confirms a successful reading or gives feedback. This does not prove an exception exists, prove a control failed, or validate a collector. It confirms only that the accepted proposition says what the specialist intended.

Potential benefits

  • Helps practitioners keep “missing,” “failed,” “stale,” and “not applicable” distinct instead of collapsing them into one ambiguous alert state.
  • Gives control and compliance teams a stable rule specification for regression tests and monitoring changes.
  • Retains the evidence-role and premise order needed for reproducible reviews.
  • Supports clearer hand-offs between automated observation and accountable human disposition.

Limits/adoption considerations

Type checking does not validate evidence authenticity, population completeness, sampling methodology, threshold suitability, control effectiveness, or residual-risk acceptance. Proposition checking is not proof completion: a well-typed implication supplies no proof that its premises hold in a period. User acceptance is not an audit sign-off. Collector hardening, clock and period alignment, tamper evidence, privacy minimization, retention, access segregation, false-positive analysis, and manual override review require independent controls.
03 Third-party compliance oversight Explore pattern

System/use case

A third-party oversight application formalizes due-diligence prerequisites, obligation flow-down, evidence refresh, risk-tier escalation, and exception-approval boundaries across vendors, outsourced services, subcontractors, and data processors. It is intended to clarify what must be reviewed before onboarding, renewal, material change, or continued use.

Operational setting

Procurement or service owners initiate a third-party record. Approved sources and questionnaires provide identity, ownership, service, data-use, location, dependency, and risk data. Compliance, security, privacy, resilience, legal, and business owners contribute decisions. Cases route by service criticality and risk tier; downstream systems consume only authorized decisions.

Decision/claim boundary

The formal proposition can define review prerequisites and escalation paths; it cannot establish beneficial ownership, verify questionnaire answers, interpret contractual language, assess sanctions or misconduct risk, or decide that residual risk is acceptable. The relevant compliance subject-matter owner approves its portion, and the designated business or risk acceptance authority owns the final decision.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every third party and service, if the service risk tier is high and due-diligence evidence is incomplete, then onboarding approval remains pending.
  • For every material service change, if the approved risk scope changes, then the third-party assessment requires refresh.
  • For every approved exception, if its review date has passed, then the exception requires reassessment.

Example architecture

A third-party master provides stable identities and record ownership. Workflow collects questionnaires, assessments, contract metadata, screening results, and exception decisions into a provenance-rich evidence graph. A policy engine controls routing and approval flags. FF Scribe supports governed rule and exception-template design, linking confirmed propositions to risk taxonomy, assessment version, evidence definitions, and reviewers. Onboarding and access still require authenticated approval. Model input is minimized to the statement and reviewed setup.

Where verified readback fits

A third-party risk professional describes an intended prerequisite or reassessment rule. A model proposes a proposition using the setup’s finite domain lexicon, and Agda checks whether it is well typed. The readback engine—not the model—then either produces the audited candidate family for supported structure or fails visibly. The practitioner accepts a successful reading or corrects it through feedback. Confirmation does not verify third-party facts, complete due diligence, prove compliance, or grant approval.

Potential benefits

  • Clarifies which evidence, risk classification, and review event drives each workflow state.
  • Makes expired exceptions and material-change triggers visible and testable.
  • Preserves a traceable separation between source facts, automated routing, specialist assessments, and risk acceptance.
  • Helps multiple oversight functions review shared propositions without forcing one function’s vocabulary to stand in for another’s judgment.

Limits/adoption considerations

Real-world identity, ownership, external data quality, contract meaning, service criticality, and risk assessment remain factual or professional judgments. A type-correct rule may still encode an unsuitable threshold or omit a material risk. No proof of due-diligence completion follows from checking a proposition type. Practitioner acceptance confirms semantic intent only, not authority or risk acceptance. Data-transfer restrictions, confidentiality, retention, purpose limitation, conflict management, override governance, and ongoing monitoring must be designed separately.
04 Compliance issue remediation and closure assurance Explore pattern

System/use case

An issue-management and assurance workspace formalizes the lifecycle from identified deficiency through action plan, evidence collection, management validation, independent retest, oversight communication, and closure decision. It is designed to prevent “action completed” from being treated as equivalent to “issue remediated and independently closed.”

Operational setting

Issues originate from monitoring, testing, audit, incidents, complaints, or management. Issue owners propose actions; control owners supply evidence; validation or audit teams test independently; a governance forum reviews material delays, residual exposure, and closure recommendations. Records retain scope changes, reopenings, superseded evidence, and approvals.

Decision/claim boundary

A checked proposition may define necessary workflow transitions, such as when retesting can begin or closure can be presented to the closure authority. It does not prove remediation effectiveness, validate test design, determine issue severity, accept residual risk, or issue an audit opinion. Management owns remediation; an explicitly named compliance, risk, or audit authority owns validation and closure according to the organization’s governance model.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every remediation action, if implementation evidence is approved by the action owner, then the action is eligible for independent retesting.
  • For every issue, if a material deficiency remains unresolved, then the issue is not eligible for closure review.
  • For every closure recommendation, if independent retesting is complete and required oversight communication is recorded, then the recommendation is eligible for closure-authority review.

Example architecture

A case platform versions issues, findings, controls, actions, owners, dates, evidence, test plans, results, communications, and decisions. A governed repository records evidence integrity and access metadata. Workflow enforces role separation and prevents skipped stages. FF Scribe supports review of transition guards and closure-readiness statements; accepted types and readings link to configurations, tests, and approval packages. Role-based authorization and accountable human decisions control closure.

Where verified readback fits

A remediation or assurance professional states the intended transition condition in natural language. The model proposes a single setup-scoped Agda proposition, and Agda checks syntax and types. If the partial readback implementation supports that structure, it generates the finite deterministic family; unsupported translation fails visibly. The professional accepts a successful reading or provides feedback. This confirms a shared reading of the statement, not remediation, proof of effectiveness, test completion, or closure approval.

Potential benefits

  • Establishes precise distinctions among action completion, management validation, independent retest, recommendation, and authoritative closure.
  • Exposes missing evidence and segregation-of-duties premises during workflow design.
  • Produces stable, auditable specifications for lifecycle configuration and regression tests.
  • Improves governance reporting by tying a status label to an explicitly confirmed proposition rather than an informal description.

Limits/adoption considerations

Type correctness does not establish issue severity, factual completion, remediation sustainability, test quality, control effectiveness, or the validity of a closure conclusion. FF Scribe does not construct proofs that workflow premises hold, and deterministic readback does not convert evidence into assurance. A user’s meaning confirmation is distinct from approval, risk acceptance, and audit authority. Independence rules, evidence retention, reopen criteria, overdue escalation, scope changes, privileged material, and assurance methodology must remain governed and tested outside the formalization loop.

Applicability frame

MLTTDB can provide a typed validation layer for reviewed compliance records. Proof-assistant source owns row types, table declarations, and semantic predicates; the SQLite term store owns ordered proof-language rows, UUIDs, projection values, database language metadata, and stored table definitions. Agda, Lean, or Rocq performs checking, even when the store launches the process. Current Agda supports finite UUID lookup in stored bodies; current Lean and Rocq preprocessors do not. Evidence collection, source-system reconciliation, IAM, case management, time evaluation, workflow approvals, retention enforcement, and audit-record immutability are external production concerns. A successful check says only that encoded terms satisfy the reviewed formalization.

Current data mode checks fetched rows as separate definitions; it does not expose a table to application proofs as an enumerable, first-class collection. Whenever an example below claims whole-snapshot coverage, uniqueness, or graph acyclicity, the architecture therefore assumes either a finite domain declared in proof source or an external snapshot compiler that emits a reconciled aggregate manifest/certificate term. The proof assistant checks that aggregate term, while external reconciliation establishes that it represents the table export supplied for review.

01 Control and evidence readiness register Explore pattern

Operational context

An enterprise prepares recurring assurance reviews across access management, change control, backup recovery, vulnerability management, and operational resilience. Each control has an owner, scope, frequency, evidence sources, sampling method, and exception policy. Governance teams struggle to tell whether an apparently complete evidence package actually covers every in-scope system and review period, and whether exclusions are legitimate rather than silent gaps.

Why MLTTDB fits

The control design and completeness rules are relatively stable, while control instances, evidence descriptors, and scope assignments change each cycle. MLTTDB can hold the reviewed instances as typed terms and rerun a proof model that distinguishes present evidence, not-applicable determinations, failed controls, and approved exceptions. Stable UUIDs support cross-references from workpapers without making the term store the system of record for evidence files.

Example architecture

GRC scope + CMDB + IAM + ticket/evidence repositories
                          |
      external collection and reconciliation service
                          v
        candidate evidence-descriptor workspace
                          |
      reviewer-approved MLTTDB term records
                          |
   store-owned verification / scheduled CI check
                          v
             proof-assistant result
                          |
      GRC workpaper, findings, and sign-off flow

The collector resolves systems, periods, and evidence locations, calculates hashes where required, and reports unmatched source items. Compliance analysts review its proposed proof-language descriptors before import. The proof repository defines scope coverage, permitted dispositions, and freshness as an explicit modeled input. Store-owned verification selects a compatible backend and returns subprocess output; the GRC platform retains assignments, comments, approvals, and workpapers.

Representative typed artifacts

Types might include ControlObjective, ScopeUnit, ReviewPeriod, EvidenceKind, EvidenceDescriptor, and ControlDisposition. Tables such as inScopeAssets :T: ScopeUnit, requiredEvidence :T: EvidenceRequirement, and assessments :T: ControlAssessment hold the row-level terms. A separately generated ControlCoverageManifest materializes the applicable asset/control pairs and their selected dispositions as one aggregate term, with the table-export digest used by the collector’s reconciliation. A descriptor can include an external object identifier, captured digest, collection instant supplied as data, and a typed relation to the requirement it purports to support. The underlying evidence remains in its governed repository.

Checks and evidence

Against that reconciled aggregate manifest, the proof assistant can establish modeled scope completeness, reject a disposition that lacks the required reason class, require a compensating-control witness for specified exception categories, and ensure an evidence descriptor matches the control’s accepted evidence kind and supplied review period. It can also prove that each required pair in the manifest is uniquely addressed. The audit packet should combine table exports, proof source revision, checker/toolchain version, process output, collector reconciliation statistics, source hashes, and reviewer decisions. MLTTDB does not verify that a screenshot is authentic, an API response is truthful, a timestamp reflects current time, or the declared population is complete.

Potential benefits

Readiness review becomes a check of explicit coverage claims rather than spreadsheet conventions. Missing and multiply classified scope items can surface early, while proof failures identify the precise modeled obligation affected by a control or scope change. Durable row identities make findings and remediation items easier to trace across review cycles.

Deployment boundary

Deploy as a periodic assurance workspace operating on reviewed snapshots. Do not use MLTTDB as the evidence vault, GRC workflow, or immutable audit log. External access controls, record retention, source attestation, and segregation of duties remain required. Control owners and qualified reviewers must approve the formal mapping and independently assess evidence quality before relying on the generated readiness result.
02 Third-party risk exception portfolio Explore pattern

Operational context

A procurement and third-party risk function manages suppliers that cannot meet one or more baseline requirements, such as encryption posture, recovery objectives, subcontractor transparency, or vulnerability remediation periods. Exceptions differ by service criticality, data classification, jurisdiction, compensating controls, accountable owner, and exit condition. Portfolio reviewers need to find exceptions whose rationale is structurally incompatible with the risk, overlaps a prohibited use, or lacks a valid remediation path.

Why MLTTDB fits

Exception governance is a finite classification problem with meaningful dependencies: a supplier service has a risk tier; that tier determines admissible exception classes; each class requires particular mitigations and approvals. MLTTDB can store reviewed exception terms while the proof source expresses those admissibility relationships. In Agda, an exception row can use literal UUID lookup to refer to an earlier stored supplier or control row, providing checked finite-domain links; equivalent Lean or Rocq designs need self-contained or ordinarily generated references because their preprocessors lack that lookup.

Example architecture

vendor inventory + assessments + contracts + case system
                          |
      external portfolio reconciler and classifier
                          v
    segregated exception review database in MLTTDB
                          |
      analyst edits and two-stage human review
                          |
             proof validation job
                          v
        exception consistency report
                          |
   external approval, monitoring, and renewal workflow

The reconciler proposes typed supplier-service, finding, and mitigation rows while preserving links to source records and reporting missing joins. Analysts resolve ambiguity; MLTTDB does not classify raw questionnaires on its own. A proof checker validates the reviewed portfolio. The case system owns state transitions, reminders, approval authority, expiration processing, and notification.

Representative typed artifacts

Candidate types include ServiceProfile tier dataClass, Requirement, Gap requirement, Mitigation gap, ExceptionClass, and ExceptionCase. Tables might be services :T: ServiceProfile, openGaps :T: Gap, and exceptions :T: ExceptionCase. An ExceptionPortfolioManifest aggregate term, built by the reconciler and matched to the source portfolio and row UUIDs, enumerates services, gaps, mitigations, and exceptions for portfolio-wide checks. An exception term can carry a mitigation set together with proof that the set satisfies the modeled minimum for its risk tier. An exit plan can be indexed by an allowed disposition such as remediate, replace, or formally accept, without claiming that the plan has been executed.

Checks and evidence

Validation can reject prohibited combinations, such as a high-criticality service using a mitigation class permitted only for low-impact data; require named owner and approved decision class; ensure every modeled gap is addressed once; and require an exit-plan shape for non-permanent dispositions. It can flag structural inconsistency when supplier tier or data use changes. Evidence should include source reconciliation, assessment and contract references, typed snapshot, checker output, policy-model revision, and separate approval records. Supplier truthfulness, contract interpretation, current control operation, real-world remediation progress, and deadline passage remain external determinations.

Potential benefits

Portfolio decisions become comparable across reviewers because exception categories and required mitigations are explicit. A policy change can be replayed against the entire reviewed portfolio, revealing cases needing reconsideration. Formal checking also reduces accidental acceptance of incomplete case structures while preserving human ownership of risk judgment.

Deployment boundary

Use MLTTDB as a decision-support and consistency-checking component, not the vendor master, contracting platform, or automatic risk-acceptance engine. Feed only reviewed, access-controlled snapshots and keep confidential evidence in appropriate repositories. Risk owners, procurement, security, privacy, and counsel must review cases according to their authority; a proof success cannot authorize an exception or determine legal adequacy.
03 Retention and legal-hold obligation map Explore pattern

Operational context

An information-governance team maps record classes to repositories, business purposes, retention schedules, disposition triggers, residency constraints, and active legal holds. The difficult cases involve overlapping obligations: a standard deletion date may be suspended by a hold, a record may inherit multiple classification rules, or a migration may change the system responsible for executing disposition. Reviewers need assurance that the modeled precedence rules yield a valid handling obligation for every declared record population.

Why MLTTDB fits

The relationships among record classes, triggers, schedules, and holds can be stated as typed rules, while the current catalog of applications and declared populations is data. MLTTDB can preserve that catalog as ordered proof-language records. The reconciliation adapter also materializes an ObligationMapManifest aggregate term from the same export, allowing the checker to evaluate precedence, coverage, and compatibility over the represented snapshot. It is especially useful for validating obligation models before they are translated into platform-specific lifecycle policies.

Example architecture

records inventory + schedule library + matter/hold system
                        |
    external authoritative-data reconciliation
                        v
   governance staging and counsel review workspace
                        |
           MLTTDB obligation terms
                        |
      project-owned proof validation in CI
                        v
   checked obligation-map artifact and diagnostics
                        |
  external lifecycle-policy compiler and enforcement

Source adapters retain the source IDs and effective-date inputs and explicitly report unresolved mappings. Governance specialists and counsel approve the semantic classification. Proof source defines precedence and compatibility at an abstract level; the term store holds selected schedules, populations, and hold relationships. A lifecycle compiler later converts approved outcomes into native repository policies, with independent tests and reconciliation.

Representative typed artifacts

Useful types include RecordClass, Repository, RetentionTrigger, Schedule, Hold, Population, and HandlingObligation. Tables can include populations :T: Population, schedules :T: ScheduleAssignment, and activeHoldDeclarations :T: HoldDeclaration. The aggregate ObligationMapManifest enumerates the population, assignment, and active-hold UUIDs and carries the inventory-export digest used for external reconciliation. A handling artifact may prove that its selected schedule is permitted for the record class and that any supplied hold suspends only the modeled disposition action while preservation controls remain specified. Calendar dates and jurisdictional facts are explicit input values, not facts inferred by MLTTDB.

Checks and evidence

Over the reconciled obligation manifest, the checker can require every enumerated in-scope population to have a unique base schedule, reject incompatible triggers, establish that hold precedence is represented for affected populations, and ensure that no modeled disposition plan bypasses an active hold declaration in the represented snapshot. It can check migration mappings for preservation of obligation classification. Evidence includes legal/policy source references, inventory and manifest reconciliation, approved effective-date snapshot, proof result, model revision, and lifecycle compiler tests. MLTTDB does not interpret law, discover records, determine whether a hold is active, calculate trustworthy current dates, or prove that downstream deletion and preservation occurred.

Potential benefits

Typed obligation mapping makes precedence assumptions visible before policies reach heterogeneous repositories. Rechecking can reveal which populations are affected by a revised schedule or hold classification, and stable identities improve traceability from policy sources through technical mappings. Diagnostics give governance and platform teams a shared, precise account of gaps.

Deployment boundary

Keep MLTTDB upstream of enforcement and downstream of qualified legal and records-management interpretation. Legal-hold issuance, custodial scope, notification, evidence preservation, and release remain in authorized systems and workflows. The term store is not an immutable recordkeeping platform. Counsel and records professionals must approve the model and each material interpretation; repository owners must verify generated policies and execution outcomes.
04 Model-governance release gate dossier Explore pattern

Operational context

A model-risk function reviews analytical and machine-learning models before initial release and material change. A dossier covers intended use, prohibited use, data lineage, validation findings, performance thresholds, monitoring, human oversight, limitations, and outstanding conditions. Teams need to know whether a release package contains the required disposition for each finding and whether its declared use remains within the reviewed operating envelope.

Why MLTTDB fits

Release criteria can be encoded as typed relationships among model class, use case, risk tier, validation test, finding, mitigation, and approval condition. MLTTDB can store the current dossier entries and ask a proof assistant to check structural completeness and modeled consistency. This connects change evidence to an explicit formal policy without asking the store to score a model or decide whether release is acceptable.

Example architecture

model registry + lineage catalog + validation reports + tickets
                           |
     external dossier assembler and source reconciler
                           v
          controlled MLTTDB review snapshot
                           |
   proof check on proposed release / material change
                           v
   machine-checkable completeness and consistency result
                           |
    model-risk committee workflow and release service
                           |
      deployment, monitoring, and incident controls

The assembler creates candidates from authoritative repositories and produces reconciliation exceptions; it does not evaluate test quality. The formal policy repository owns types and gates. MLTTDB stores reviewed terms, identifiers, and order. A store endpoint may orchestrate the selected proof process, while the committee workflow records deliberation and the release service enforces actual deployment authorization.

Representative typed artifacts

Types might include ModelClass, IntendedUse, RiskTier, ValidationRequirement, TestResult, Finding severity, Disposition, and ReleaseCase. Tables such as requirements :T: ValidationRequirement, findings :T: Finding, and releaseConditions :T: ReleaseCondition can represent which evidence shapes are required for a given class. A ModelReleaseDossierManifest aggregate term, reconciled to registry, validation, finding, and release-condition exports, enumerates the requirement and finding UUIDs covered by the release-wide argument. A release case may carry proofs that all blocking finding identifiers represented there have approved modeled dispositions and that the selected use case refines the reviewed intended-use envelope.

Checks and evidence

Validation can establish completeness over the explicitly supplied requirements, reject contradictory finding dispositions, require monitoring metrics for selected risk tiers, and ensure conditional approvals have a corresponding control and accountable role in the model. Regression checks can replay a policy change across pending dossiers. The evidence bundle should bind terms to registry version, data and code references, independent validation report, model-card revision, checker output, and committee record. Performance validity, data representativeness, fairness, robustness, monitoring operation, and human approval are not established merely because dossier terms type-check.

Potential benefits

The release gate gains a consistent vocabulary and an executable completeness argument. Reviewers can focus on the substance and assumptions of evidence rather than repeatedly identifying missing dossier sections. When policy or model classification changes, affected conditions fail explicitly and can be routed for reassessment.

Deployment boundary

Deploy as a pre-release evidence check, not a production inference gateway or autonomous committee. Keep model artifacts and sensitive validation data in their governed repositories, with MLTTDB containing only reviewed terms and references appropriate to its access tier. Qualified validators, model owners, risk officers, security/privacy specialists, and the authorized decision body retain responsibility for adequacy and release approval.

These read-only, pan-and-zoom models expose three abstraction levels for each workflow. They are explanatory examples, not live operational or decision systems.

01

Incident-to-audit evidence

About this workflow

This example represents the evidence chain that connects an operational or security incident to an audit-ready control conclusion. Response teams must restore safe service quickly, but compliance and audit also need to know what happened, which obligations were triggered, who approved key actions, whether controls were restored, and where the supporting records came from. The workflow treats evidence capture as part of response rather than a retrospective document exercise.

The normal path starts when the alert, affected control context, initial logs, and reporter observations are preserved. Triage assesses severity, scope, notification or reporting obligations, and assigns both response and evidence owners. During containment, approved actions and their commands, approvals, timestamps, and collected artifacts are recorded. Remediation removes the cause and links system changes to tested corrective requirements. Control validation then tests restored and compensating controls and reconciles expected evidence with observed results. When validation passes, the timeline, decisions, artifact lineage, limitations, and conclusion statements are assembled into an audit package with appropriate retention and access approval.

Exception handling acknowledges that incident evidence is often incomplete or contradictory. A gap discovered in triage or containment enters a dedicated evidence-exception path instead of being silently noted at closure. Missing, conflicting, or inaccessible records receive recovery actions and a documented limitation. Recovered evidence returns to control validation so the conclusion is tested against the improved record. If the gap is fundamental, the response must be reconstructed from available sources and returned to triage. Remediation regression sends the case back to containment; failed validation sends it back to remediation. Even a prepared audit package can be reopened if a packaging gap reveals that its conclusion is not adequately supported.

These controls matter because an incident can expose both an operational failure and a failure of the control environment. Preserving provenance, approvals, test results, and known limitations allows management, regulators, customers, and auditors to distinguish fact from assumption. It also reduces reliance on memories or manually reconstructed timelines and ensures that technical recovery is not mistaken for demonstrated control effectiveness.

Layer 1 — Incident evidence lifecycle

This layer shows the complete evidentiary outcome from detection through triage, containment, remediation, validation, and audit-ready closure. It is designed for incident governance, compliance leadership, and auditors assessing whether response and control conclusions are supportable. It intentionally omits individual commands, artifacts, test cases, and evidence-owner assignments.

Layer 2 — Response evidence operations

This layer presents the coordinated response and evidence work: preserve, triage, contain, remediate, validate, package, and resolve evidence exceptions. It includes the important loops for record gaps, remediation regression, validation failure, evidence recovery, reconstruction, and package deficiencies. It excludes tool-specific response procedures, notification deadlines, and the precise audit workpaper format.

Layer 3 — Evidence checks and actions

This layer covers the concrete records and checks inside each stage: register alerts and control context, preserve logs, assess scope and obligations, assign owners, record commands and approvals, link corrective changes to requirements, test restored and compensating controls, reconcile evidence, document missing records, assemble artifact lineage, and approve retention and conclusions. It supports procedure, evidence-schema, and automation design while intentionally not specifying a security platform, incident taxonomy, forensic technique, regulatory regime, or retention duration.
02

Privileged access recertification

About this workflow

This example represents a periodic recertification of administrator, elevated, and other high-impact access. The objective is not merely to collect attestations. It is to establish a complete review population, connect accounts to accountable identities and role sources, obtain informed decisions from business or system owners, execute required removals, and prove that approved decisions match effective access at the end of the review period.

The standard path begins by defining the systems, privileged roles, review period, policy criteria, and accountable owners. Entitlements are collected from directories and target platforms, then reconciled to people, service identities, and authoritative role records. Owners receive enough context to make a meaningful retain, modify, or revoke decision, including stated business need and recent-use evidence. Revocations and privilege reductions are issued through controlled change requests and verified across dependent systems. Retained and remediated access converges in control reconciliation, where recorded decisions are compared with actual access. Certification occurs only when the review population, decisions, and remediation are complete and the evidence package can be sealed.

The exception routes address common access-governance weaknesses. An inventory gap returns to scope because an incomplete population cannot support certification. Orphaned accounts, disputed ownership, emergency access, or decisions that cannot be completed enter an access-exception process with compensating controls and expiry. Failed removals also become exceptions rather than disappearing into an operations queue. Insufficient exception evidence returns to the owner decision. Residual access found during reconciliation reopens removal, ensuring that a closed ticket is not mistaken for an effective revocation.

These controls matter because privileged access can bypass preventive controls, alter evidence, and materially affect systems or data. A well-designed recertification demonstrates completeness, informed accountability, least privilege, timely remediation, and a defensible treatment of exceptions. It also distinguishes access that was approved on paper from access that remained technically active.

Layer 1 — Access recertification lifecycle

This layer shows the control from scoped review to certified conclusion, with remediation and exceptions visible as governed outcomes. It is aimed at control owners, risk committees, and auditors deciding whether the periodic review operated effectively. It intentionally omits connector behavior, account-level evidence, owner prompts, and individual access-change tasks.

Layer 2 — Privileged access review operations

This layer presents the compliance work queues: scoping, inventory collection, owner decision, removal execution, exception handling, reconciliation, and certification. It includes loops for population gaps, disputed access, failed revocation, inadequate evidence, and residual privilege. It excludes platform-specific entitlement models, campaign tooling, and detailed approval matrices.

Layer 3 — Control checks and actions

This layer identifies the concrete tests and records needed to operate the control: select systems and roles, identify owners, collect entitlements, reconcile identities, present business need and usage, capture decisions, issue least-privilege changes, verify dependent systems, set compensating controls and expiry, compare decisions with effective access, and seal evidence. It supports procedure and automation design while intentionally not prescribing an identity-governance product, directory schema, policy frequency, or organization-specific role catalogue.
03

Third-party compliance oversight

About this workflow

This example represents risk-based oversight of a vendor or other third party from proposed engagement through governed service, remediation, and exit. It recognizes that due diligence is not a one-time questionnaire. Compliance obligations must be translated into contract controls, monitored while the service operates, revisited when risk changes, and closed with evidence that access, assets, data, and residual obligations were handled appropriately.

The ordinary path starts by classifying the service, data handled, jurisdictions, subcontracting exposure, and accountable internal owners. Due diligence collects and assesses evidence such as beneficial ownership, sanctions screening, security controls, conduct indicators, licenses, and assurance reports. Requirements that pass assessment are converted into enforceable agreement terms covering control performance, notification, assurance, audit rights, and cooperation. The service then enters ongoing monitoring, where current attestations, performance indicators, adverse events, and changes in obligations are reviewed. A planned exit ends service access, recovers managed assets, and retains closure approval along with any surviving confidentiality, retention, or regulatory duties.

The exception paths avoid the false choice between unconditional approval and immediate termination. A due-diligence gap or missing contract control enters risk exception, where the unmet requirement, exposure, compensating controls, accountable approver, and expiry are recorded. An approved exception permits monitored operation; an exception that needs stronger controls moves into remediation. Monitoring findings also trigger a corrective-action plan with owners and dates. Completed actions return to monitoring only after evidence is verified. Failed remediation routes to exit, making termination a defined control outcome rather than an improvised response. Any later re-engagement begins again with current scope instead of inheriting stale assurance.

These controls matter because the organization remains accountable for many obligations performed through third parties. A traceable lifecycle helps compliance, procurement, information security, legal, and business owners distinguish inherent risk, contractual commitments, operating evidence, accepted residual risk, and unresolved control failure. It also prevents expired exceptions or old attestations from being treated as permanent approval.

Layer 1 — Third-party oversight lifecycle

This layer shows the engagement’s governance outcome from initial scope to monitored service or controlled exit. It is useful for accountable executives, risk owners, and oversight committees reviewing whether the third party remains within appetite. It intentionally omits individual questionnaire responses, contract clauses, monitoring metrics, and remediation tasks.

Layer 2 — Vendor compliance operations

This layer presents the cross-functional operating stages: scope, due diligence, contract controls, monitoring, remediation, exception management, and exit. It makes the decision routes for evidence gaps, contract gaps, adverse findings, accepted exceptions, failed remediation, and re-engagement explicit. It excludes jurisdiction-specific tests, sourcing workflow details, and the exact roles in a firm’s approval authority.

Layer 3 — Oversight checks and actions

This layer describes the concrete activities: classify service and data exposure, assign obligations and owners, collect ownership and control evidence, assess sanctions and conduct indicators, draft assurance and notification terms, review current attestations, define corrective actions, verify closure evidence, document compensating controls and expiry, revoke access, and recover assets. It supports control mapping and procedure design while deliberately remaining neutral about vendor tiering methodology, contract template, screening provider, assurance framework, and monitoring platform.
Interactive state machine

Workflow demo

Skip to content

Domains

Compliance

Placeholder domain page for compliance rules involving controls, evidence, and audit obligations.

  • controls
  • evidence
  • audits

Problems we solve

Checked boundaries and evidence

  • Controls span policies, systems, owners, evidence sources, and review periods.
  • Manual evidence collection is repetitive and difficult to reproduce.
  • Exceptions can obscure whether a control is absent, failed, or not applicable.
  • Audit conclusions must remain linked to current rules and supporting records.
Control Mapping

Connect obligations, controls, owners, and evidence sources.

Evidence Checking

Evaluate whether required records are present and current.

Exception Analysis

Classify gaps and route them through explicit review paths.

Consistency Validation

Check alignment between policy, control, and implementation.

Audit Preparation

Assemble traceable placeholder evidence and decision records.

Application patterns

Imported product records

These panels use the same generated application portfolio as the desktop workbench.

FF Scribe4 patterns
The Compliance domain links obligations, policies, controls, owners, evidence, exceptions, and audits. Beyond collecting records, teams must preserve applicability, control purpose, operating evidence, and authority to resolve gaps. These examples use FF Scribe to confirm tightly scoped propositions without making current-rule or jurisdictional claims. Interpretation, risk acceptance, control ownership, and assurance conclusions remain with accountable professionals.
01Obligation-to-control mapping and design assessment

System/use case

A compliance requirements platform formalizes mapping assertions between a governed obligation, internal policy statement, control objective, control activity, accountable owner, and evidence source. It supports new-requirement intake, control rationalization, and review of whether a proposed control description addresses the intended obligation boundary.

Operational setting

Compliance advisory teams maintain approved obligations and applicability decisions. Policy owners maintain internal standards; first-line owners document controls; second-line compliance reviews mappings and challenges gaps. Changes capture effective periods, business and product scope, rationale, and sign-off. Internal audit can use the lineage without inheriting management’s conclusion.

Decision/claim boundary

The proposition may state a mapping or review condition, such as when an applicable obligation requires an approved control and owner. It cannot decide legal applicability, interpret an obligation, establish that a control is well designed, or show that it operates effectively. The designated compliance authority owns interpretation and mapping approval; the control owner remains accountable for design and operation.

Candidate checked statements

These are illustrative controlled-English propositions for a possible setup, not capabilities or rules already implemented:

  • For every applicable obligation, if no approved control mapping is recorded, then the obligation requires compliance review.
  • For every control mapping, if the obligation scope changes, then the mapping requires reassessment.
  • For every control, if an accountable owner and an approved evidence source are recorded, then the control is eligible for design review.

Example architecture

A repository separates versioned source material from approved internal interpretations. A graph links obligation versions, applicability decisions, policies, controls, systems, owners, risks, and evidence. Workflow enforces roles and dates; impact analysis exposes downstream mappings. During rule review, FF Scribe output is stored with setup, source and mapping versions, compiler result, readback ID, and practitioner response. Only authorized reviewers approve mappings; the model cannot modify obligations or interpretations.

Where verified readback fits

An analyst describes the intended mapping or reassessment condition in natural language. The model proposes one proposition within a deliberately small setup vocabulary. Agda accepts or rejects it on syntax and type grounds. If the separate partial readback stage supports the checked structure, it emits the finite audited family with semantic-rule provenance; otherwise it fails visibly without partial prose. The analyst accepts a successful reading or provides feedback. Acceptance confirms the statement’s intended meaning; it does not make the interpretation authoritative or prove that the control addresses the obligation.

Potential benefits

  • Makes obligation, applicability, control, owner, and evidence relationships explicit for multidisciplinary review.
  • Preserves reproducible meaning across requirement-version and policy changes.
  • Improves impact analysis by attaching confirmed propositions to governed graph relationships.
  • Reduces semantic drift between compliance narratives, control libraries, engineering requirements, and audit walkthroughs.

Limits/adoption considerations

A type-correct proposition is structurally valid in the selected setup, not legally correct, factually true, or evidence of control design effectiveness. FF Scribe checks the proposition type rather than completing a proof that a mapping exists or is adequate. Practitioner confirmation establishes user intent, not approval authority. Source licensing, version provenance, privilege, interpretive governance, access control, and independent challenge remain essential. Complex exceptions, negation, disjunction, and temporal applicability require explicit supported formal structures; opaque labels should not conceal unmodeled reasoning.
02Continuous control evidence and exception triage

System/use case

A continuous compliance monitoring service formalizes the conditions under which evidence is current, a control observation is reviewable, and an exception is routed as missing, failed, stale, contradictory, or not applicable. It targets high-volume controls whose artifacts originate in identity, change, configuration, transaction, or ticketing systems.

Operational setting

Connectors collect integrity-protected evidence packages from systems of record on defined schedules. A monitoring engine evaluates completeness and freshness, records population and period, and creates exceptions. First-line owners investigate; second-line compliance reviews material or recurring deviations; internal audit can inspect provenance without adopting the monitoring conclusion.

Decision/claim boundary

The checked statement defines evidence-handling logic or an escalation boundary. It does not establish that evidence is authentic, that the tested population is complete, that the control operated as described, or that a monitoring algorithm is valid. The control owner attests to operation; the compliance oversight function approves exception taxonomy and escalation policy.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every control execution and review period, if required evidence is absent, then the execution is classified for missing-evidence review.
  • For every evidence record, if its observation period differs from the control period, then the record does not satisfy the current evidence request.
  • For every recurring exception, if the approved recurrence threshold is met, then the exception requires compliance escalation.

Example architecture

Source-specific collectors send metadata and artifacts to a write-once evidence store. A schema registry identifies control, population, period, system, collector, and integrity fields. The monitoring service evaluates configured checks and sends reason-coded cases to a workflow platform. Dashboards consume the case state, not raw unreviewed conclusions. FF Scribe supports authoring and review of classification and routing propositions, with accepted readings bound to rule versions and test fixtures. Trust is layered: collectors establish provenance, monitoring computes observations, practitioners adjudicate meaning and disposition, and independent assurance evaluates the overall design.

Where verified readback fits

A control specialist describes a classification or escalation condition. The model maps that request to a setup-scoped proposition, and Agda verifies that the candidate is a valid type in the registered vocabulary. For supported structure, the partial readback stage presents audited canonical, compact, evidence-oriented, or structured readings; unsupported translation fails visibly. The specialist explicitly confirms a successful reading or gives feedback. This does not prove an exception exists, prove a control failed, or validate a collector. It confirms only that the accepted proposition says what the specialist intended.

Potential benefits

  • Helps practitioners keep “missing,” “failed,” “stale,” and “not applicable” distinct instead of collapsing them into one ambiguous alert state.
  • Gives control and compliance teams a stable rule specification for regression tests and monitoring changes.
  • Retains the evidence-role and premise order needed for reproducible reviews.
  • Supports clearer hand-offs between automated observation and accountable human disposition.

Limits/adoption considerations

Type checking does not validate evidence authenticity, population completeness, sampling methodology, threshold suitability, control effectiveness, or residual-risk acceptance. Proposition checking is not proof completion: a well-typed implication supplies no proof that its premises hold in a period. User acceptance is not an audit sign-off. Collector hardening, clock and period alignment, tamper evidence, privacy minimization, retention, access segregation, false-positive analysis, and manual override review require independent controls.
03Third-party compliance oversight

System/use case

A third-party oversight application formalizes due-diligence prerequisites, obligation flow-down, evidence refresh, risk-tier escalation, and exception-approval boundaries across vendors, outsourced services, subcontractors, and data processors. It is intended to clarify what must be reviewed before onboarding, renewal, material change, or continued use.

Operational setting

Procurement or service owners initiate a third-party record. Approved sources and questionnaires provide identity, ownership, service, data-use, location, dependency, and risk data. Compliance, security, privacy, resilience, legal, and business owners contribute decisions. Cases route by service criticality and risk tier; downstream systems consume only authorized decisions.

Decision/claim boundary

The formal proposition can define review prerequisites and escalation paths; it cannot establish beneficial ownership, verify questionnaire answers, interpret contractual language, assess sanctions or misconduct risk, or decide that residual risk is acceptable. The relevant compliance subject-matter owner approves its portion, and the designated business or risk acceptance authority owns the final decision.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every third party and service, if the service risk tier is high and due-diligence evidence is incomplete, then onboarding approval remains pending.
  • For every material service change, if the approved risk scope changes, then the third-party assessment requires refresh.
  • For every approved exception, if its review date has passed, then the exception requires reassessment.

Example architecture

A third-party master provides stable identities and record ownership. Workflow collects questionnaires, assessments, contract metadata, screening results, and exception decisions into a provenance-rich evidence graph. A policy engine controls routing and approval flags. FF Scribe supports governed rule and exception-template design, linking confirmed propositions to risk taxonomy, assessment version, evidence definitions, and reviewers. Onboarding and access still require authenticated approval. Model input is minimized to the statement and reviewed setup.

Where verified readback fits

A third-party risk professional describes an intended prerequisite or reassessment rule. A model proposes a proposition using the setup’s finite domain lexicon, and Agda checks whether it is well typed. The readback engine—not the model—then either produces the audited candidate family for supported structure or fails visibly. The practitioner accepts a successful reading or corrects it through feedback. Confirmation does not verify third-party facts, complete due diligence, prove compliance, or grant approval.

Potential benefits

  • Clarifies which evidence, risk classification, and review event drives each workflow state.
  • Makes expired exceptions and material-change triggers visible and testable.
  • Preserves a traceable separation between source facts, automated routing, specialist assessments, and risk acceptance.
  • Helps multiple oversight functions review shared propositions without forcing one function’s vocabulary to stand in for another’s judgment.

Limits/adoption considerations

Real-world identity, ownership, external data quality, contract meaning, service criticality, and risk assessment remain factual or professional judgments. A type-correct rule may still encode an unsuitable threshold or omit a material risk. No proof of due-diligence completion follows from checking a proposition type. Practitioner acceptance confirms semantic intent only, not authority or risk acceptance. Data-transfer restrictions, confidentiality, retention, purpose limitation, conflict management, override governance, and ongoing monitoring must be designed separately.
04Compliance issue remediation and closure assurance

System/use case

An issue-management and assurance workspace formalizes the lifecycle from identified deficiency through action plan, evidence collection, management validation, independent retest, oversight communication, and closure decision. It is designed to prevent “action completed” from being treated as equivalent to “issue remediated and independently closed.”

Operational setting

Issues originate from monitoring, testing, audit, incidents, complaints, or management. Issue owners propose actions; control owners supply evidence; validation or audit teams test independently; a governance forum reviews material delays, residual exposure, and closure recommendations. Records retain scope changes, reopenings, superseded evidence, and approvals.

Decision/claim boundary

A checked proposition may define necessary workflow transitions, such as when retesting can begin or closure can be presented to the closure authority. It does not prove remediation effectiveness, validate test design, determine issue severity, accept residual risk, or issue an audit opinion. Management owns remediation; an explicitly named compliance, risk, or audit authority owns validation and closure according to the organization’s governance model.

Candidate checked statements

Illustrative targets for a future setup—not claims of current adapter coverage—include:

  • For every remediation action, if implementation evidence is approved by the action owner, then the action is eligible for independent retesting.
  • For every issue, if a material deficiency remains unresolved, then the issue is not eligible for closure review.
  • For every closure recommendation, if independent retesting is complete and required oversight communication is recorded, then the recommendation is eligible for closure-authority review.

Example architecture

A case platform versions issues, findings, controls, actions, owners, dates, evidence, test plans, results, communications, and decisions. A governed repository records evidence integrity and access metadata. Workflow enforces role separation and prevents skipped stages. FF Scribe supports review of transition guards and closure-readiness statements; accepted types and readings link to configurations, tests, and approval packages. Role-based authorization and accountable human decisions control closure.

Where verified readback fits

A remediation or assurance professional states the intended transition condition in natural language. The model proposes a single setup-scoped Agda proposition, and Agda checks syntax and types. If the partial readback implementation supports that structure, it generates the finite deterministic family; unsupported translation fails visibly. The professional accepts a successful reading or provides feedback. This confirms a shared reading of the statement, not remediation, proof of effectiveness, test completion, or closure approval.

Potential benefits

  • Establishes precise distinctions among action completion, management validation, independent retest, recommendation, and authoritative closure.
  • Exposes missing evidence and segregation-of-duties premises during workflow design.
  • Produces stable, auditable specifications for lifecycle configuration and regression tests.
  • Improves governance reporting by tying a status label to an explicitly confirmed proposition rather than an informal description.

Limits/adoption considerations

Type correctness does not establish issue severity, factual completion, remediation sustainability, test quality, control effectiveness, or the validity of a closure conclusion. FF Scribe does not construct proofs that workflow premises hold, and deterministic readback does not convert evidence into assurance. A user’s meaning confirmation is distinct from approval, risk acceptance, and audit authority. Independence rules, evidence retention, reopen criteria, overdue escalation, scope changes, privileged material, and assurance methodology must remain governed and tested outside the formalization loop.
MLTTDB4 patterns
These illustrative applications develop the Compliance domain brief in ~/nn-ff-web/content/domains/compliance.md: control mapping, evidence checking, exception analysis, consistency validation, and reproducible audit preparation. They are architecture candidates rather than legal conclusions or certified compliance solutions. Control owners, counsel, auditors, risk specialists, and formal-methods practitioners must review the selected obligations, evidence criteria, and proof models.
01Control and evidence readiness register

Operational context

An enterprise prepares recurring assurance reviews across access management, change control, backup recovery, vulnerability management, and operational resilience. Each control has an owner, scope, frequency, evidence sources, sampling method, and exception policy. Governance teams struggle to tell whether an apparently complete evidence package actually covers every in-scope system and review period, and whether exclusions are legitimate rather than silent gaps.

Why MLTTDB fits

The control design and completeness rules are relatively stable, while control instances, evidence descriptors, and scope assignments change each cycle. MLTTDB can hold the reviewed instances as typed terms and rerun a proof model that distinguishes present evidence, not-applicable determinations, failed controls, and approved exceptions. Stable UUIDs support cross-references from workpapers without making the term store the system of record for evidence files.

Example architecture

GRC scope + CMDB + IAM + ticket/evidence repositories
                          |
      external collection and reconciliation service
                          v
        candidate evidence-descriptor workspace
                          |
      reviewer-approved MLTTDB term records
                          |
   store-owned verification / scheduled CI check
                          v
             proof-assistant result
                          |
      GRC workpaper, findings, and sign-off flow

The collector resolves systems, periods, and evidence locations, calculates hashes where required, and reports unmatched source items. Compliance analysts review its proposed proof-language descriptors before import. The proof repository defines scope coverage, permitted dispositions, and freshness as an explicit modeled input. Store-owned verification selects a compatible backend and returns subprocess output; the GRC platform retains assignments, comments, approvals, and workpapers.

Representative typed artifacts

Types might include ControlObjective, ScopeUnit, ReviewPeriod, EvidenceKind, EvidenceDescriptor, and ControlDisposition. Tables such as inScopeAssets :T: ScopeUnit, requiredEvidence :T: EvidenceRequirement, and assessments :T: ControlAssessment hold the row-level terms. A separately generated ControlCoverageManifest materializes the applicable asset/control pairs and their selected dispositions as one aggregate term, with the table-export digest used by the collector’s reconciliation. A descriptor can include an external object identifier, captured digest, collection instant supplied as data, and a typed relation to the requirement it purports to support. The underlying evidence remains in its governed repository.

Checks and evidence

Against that reconciled aggregate manifest, the proof assistant can establish modeled scope completeness, reject a disposition that lacks the required reason class, require a compensating-control witness for specified exception categories, and ensure an evidence descriptor matches the control’s accepted evidence kind and supplied review period. It can also prove that each required pair in the manifest is uniquely addressed. The audit packet should combine table exports, proof source revision, checker/toolchain version, process output, collector reconciliation statistics, source hashes, and reviewer decisions. MLTTDB does not verify that a screenshot is authentic, an API response is truthful, a timestamp reflects current time, or the declared population is complete.

Potential benefits

Readiness review becomes a check of explicit coverage claims rather than spreadsheet conventions. Missing and multiply classified scope items can surface early, while proof failures identify the precise modeled obligation affected by a control or scope change. Durable row identities make findings and remediation items easier to trace across review cycles.

Deployment boundary

Deploy as a periodic assurance workspace operating on reviewed snapshots. Do not use MLTTDB as the evidence vault, GRC workflow, or immutable audit log. External access controls, record retention, source attestation, and segregation of duties remain required. Control owners and qualified reviewers must approve the formal mapping and independently assess evidence quality before relying on the generated readiness result.
02Third-party risk exception portfolio

Operational context

A procurement and third-party risk function manages suppliers that cannot meet one or more baseline requirements, such as encryption posture, recovery objectives, subcontractor transparency, or vulnerability remediation periods. Exceptions differ by service criticality, data classification, jurisdiction, compensating controls, accountable owner, and exit condition. Portfolio reviewers need to find exceptions whose rationale is structurally incompatible with the risk, overlaps a prohibited use, or lacks a valid remediation path.

Why MLTTDB fits

Exception governance is a finite classification problem with meaningful dependencies: a supplier service has a risk tier; that tier determines admissible exception classes; each class requires particular mitigations and approvals. MLTTDB can store reviewed exception terms while the proof source expresses those admissibility relationships. In Agda, an exception row can use literal UUID lookup to refer to an earlier stored supplier or control row, providing checked finite-domain links; equivalent Lean or Rocq designs need self-contained or ordinarily generated references because their preprocessors lack that lookup.

Example architecture

vendor inventory + assessments + contracts + case system
                          |
      external portfolio reconciler and classifier
                          v
    segregated exception review database in MLTTDB
                          |
      analyst edits and two-stage human review
                          |
             proof validation job
                          v
        exception consistency report
                          |
   external approval, monitoring, and renewal workflow

The reconciler proposes typed supplier-service, finding, and mitigation rows while preserving links to source records and reporting missing joins. Analysts resolve ambiguity; MLTTDB does not classify raw questionnaires on its own. A proof checker validates the reviewed portfolio. The case system owns state transitions, reminders, approval authority, expiration processing, and notification.

Representative typed artifacts

Candidate types include ServiceProfile tier dataClass, Requirement, Gap requirement, Mitigation gap, ExceptionClass, and ExceptionCase. Tables might be services :T: ServiceProfile, openGaps :T: Gap, and exceptions :T: ExceptionCase. An ExceptionPortfolioManifest aggregate term, built by the reconciler and matched to the source portfolio and row UUIDs, enumerates services, gaps, mitigations, and exceptions for portfolio-wide checks. An exception term can carry a mitigation set together with proof that the set satisfies the modeled minimum for its risk tier. An exit plan can be indexed by an allowed disposition such as remediate, replace, or formally accept, without claiming that the plan has been executed.

Checks and evidence

Validation can reject prohibited combinations, such as a high-criticality service using a mitigation class permitted only for low-impact data; require named owner and approved decision class; ensure every modeled gap is addressed once; and require an exit-plan shape for non-permanent dispositions. It can flag structural inconsistency when supplier tier or data use changes. Evidence should include source reconciliation, assessment and contract references, typed snapshot, checker output, policy-model revision, and separate approval records. Supplier truthfulness, contract interpretation, current control operation, real-world remediation progress, and deadline passage remain external determinations.

Potential benefits

Portfolio decisions become comparable across reviewers because exception categories and required mitigations are explicit. A policy change can be replayed against the entire reviewed portfolio, revealing cases needing reconsideration. Formal checking also reduces accidental acceptance of incomplete case structures while preserving human ownership of risk judgment.

Deployment boundary

Use MLTTDB as a decision-support and consistency-checking component, not the vendor master, contracting platform, or automatic risk-acceptance engine. Feed only reviewed, access-controlled snapshots and keep confidential evidence in appropriate repositories. Risk owners, procurement, security, privacy, and counsel must review cases according to their authority; a proof success cannot authorize an exception or determine legal adequacy.
03Retention and legal-hold obligation map

Operational context

An information-governance team maps record classes to repositories, business purposes, retention schedules, disposition triggers, residency constraints, and active legal holds. The difficult cases involve overlapping obligations: a standard deletion date may be suspended by a hold, a record may inherit multiple classification rules, or a migration may change the system responsible for executing disposition. Reviewers need assurance that the modeled precedence rules yield a valid handling obligation for every declared record population.

Why MLTTDB fits

The relationships among record classes, triggers, schedules, and holds can be stated as typed rules, while the current catalog of applications and declared populations is data. MLTTDB can preserve that catalog as ordered proof-language records. The reconciliation adapter also materializes an ObligationMapManifest aggregate term from the same export, allowing the checker to evaluate precedence, coverage, and compatibility over the represented snapshot. It is especially useful for validating obligation models before they are translated into platform-specific lifecycle policies.

Example architecture

records inventory + schedule library + matter/hold system
                        |
    external authoritative-data reconciliation
                        v
   governance staging and counsel review workspace
                        |
           MLTTDB obligation terms
                        |
      project-owned proof validation in CI
                        v
   checked obligation-map artifact and diagnostics
                        |
  external lifecycle-policy compiler and enforcement

Source adapters retain the source IDs and effective-date inputs and explicitly report unresolved mappings. Governance specialists and counsel approve the semantic classification. Proof source defines precedence and compatibility at an abstract level; the term store holds selected schedules, populations, and hold relationships. A lifecycle compiler later converts approved outcomes into native repository policies, with independent tests and reconciliation.

Representative typed artifacts

Useful types include RecordClass, Repository, RetentionTrigger, Schedule, Hold, Population, and HandlingObligation. Tables can include populations :T: Population, schedules :T: ScheduleAssignment, and activeHoldDeclarations :T: HoldDeclaration. The aggregate ObligationMapManifest enumerates the population, assignment, and active-hold UUIDs and carries the inventory-export digest used for external reconciliation. A handling artifact may prove that its selected schedule is permitted for the record class and that any supplied hold suspends only the modeled disposition action while preservation controls remain specified. Calendar dates and jurisdictional facts are explicit input values, not facts inferred by MLTTDB.

Checks and evidence

Over the reconciled obligation manifest, the checker can require every enumerated in-scope population to have a unique base schedule, reject incompatible triggers, establish that hold precedence is represented for affected populations, and ensure that no modeled disposition plan bypasses an active hold declaration in the represented snapshot. It can check migration mappings for preservation of obligation classification. Evidence includes legal/policy source references, inventory and manifest reconciliation, approved effective-date snapshot, proof result, model revision, and lifecycle compiler tests. MLTTDB does not interpret law, discover records, determine whether a hold is active, calculate trustworthy current dates, or prove that downstream deletion and preservation occurred.

Potential benefits

Typed obligation mapping makes precedence assumptions visible before policies reach heterogeneous repositories. Rechecking can reveal which populations are affected by a revised schedule or hold classification, and stable identities improve traceability from policy sources through technical mappings. Diagnostics give governance and platform teams a shared, precise account of gaps.

Deployment boundary

Keep MLTTDB upstream of enforcement and downstream of qualified legal and records-management interpretation. Legal-hold issuance, custodial scope, notification, evidence preservation, and release remain in authorized systems and workflows. The term store is not an immutable recordkeeping platform. Counsel and records professionals must approve the model and each material interpretation; repository owners must verify generated policies and execution outcomes.
04Model-governance release gate dossier

Operational context

A model-risk function reviews analytical and machine-learning models before initial release and material change. A dossier covers intended use, prohibited use, data lineage, validation findings, performance thresholds, monitoring, human oversight, limitations, and outstanding conditions. Teams need to know whether a release package contains the required disposition for each finding and whether its declared use remains within the reviewed operating envelope.

Why MLTTDB fits

Release criteria can be encoded as typed relationships among model class, use case, risk tier, validation test, finding, mitigation, and approval condition. MLTTDB can store the current dossier entries and ask a proof assistant to check structural completeness and modeled consistency. This connects change evidence to an explicit formal policy without asking the store to score a model or decide whether release is acceptable.

Example architecture

model registry + lineage catalog + validation reports + tickets
                           |
     external dossier assembler and source reconciler
                           v
          controlled MLTTDB review snapshot
                           |
   proof check on proposed release / material change
                           v
   machine-checkable completeness and consistency result
                           |
    model-risk committee workflow and release service
                           |
      deployment, monitoring, and incident controls

The assembler creates candidates from authoritative repositories and produces reconciliation exceptions; it does not evaluate test quality. The formal policy repository owns types and gates. MLTTDB stores reviewed terms, identifiers, and order. A store endpoint may orchestrate the selected proof process, while the committee workflow records deliberation and the release service enforces actual deployment authorization.

Representative typed artifacts

Types might include ModelClass, IntendedUse, RiskTier, ValidationRequirement, TestResult, Finding severity, Disposition, and ReleaseCase. Tables such as requirements :T: ValidationRequirement, findings :T: Finding, and releaseConditions :T: ReleaseCondition can represent which evidence shapes are required for a given class. A ModelReleaseDossierManifest aggregate term, reconciled to registry, validation, finding, and release-condition exports, enumerates the requirement and finding UUIDs covered by the release-wide argument. A release case may carry proofs that all blocking finding identifiers represented there have approved modeled dispositions and that the selected use case refines the reviewed intended-use envelope.

Checks and evidence

Validation can establish completeness over the explicitly supplied requirements, reject contradictory finding dispositions, require monitoring metrics for selected risk tiers, and ensure conditional approvals have a corresponding control and accountable role in the model. Regression checks can replay a policy change across pending dossiers. The evidence bundle should bind terms to registry version, data and code references, independent validation report, model-card revision, checker output, and committee record. Performance validity, data representativeness, fairness, robustness, monitoring operation, and human approval are not established merely because dossier terms type-check.

Potential benefits

The release gate gains a consistent vocabulary and an executable completeness argument. Reviewers can focus on the substance and assumptions of evidence rather than repeatedly identifying missing dossier sections. When policy or model classification changes, affected conditions fail explicitly and can be routed for reassessment.

Deployment boundary

Deploy as a pre-release evidence check, not a production inference gateway or autonomous committee. Keep model artifacts and sensitive validation data in their governed repositories, with MLTTDB containing only reviewed terms and references appropriate to its access tier. Qualified validators, model owners, risk officers, security/privacy specialists, and the authorized decision body retain responsibility for adequacy and release approval.
State Machine Studio3 demos
SMIncident-to-audit evidence

This example represents the evidence chain that connects an operational or security incident to an audit-ready control conclusion. Response teams must restore safe service quickly, but compliance and audit also need to know what happened, which obligations were triggered, who approved key actions, whether controls were restored, and where the supporting records came from. The workflow treats evidence capture as part of response rather than a retrospective document exercise.

The normal path starts when the alert, affected control context, initial logs, and reporter observations are preserved. Triage assesses severity, scope, notification or reporting obligations, and assigns both response and evidence owners. During containment, approved actions and their commands, approvals, timestamps, and collected artifacts are recorded. Remediation removes the cause and links system changes to tested corrective requirements. Control validation then tests restored and compensating controls and reconciles expected evidence with observed results. When validation passes, the timeline, decisions, artifact lineage, limitations, and conclusion statements are assembled into an audit package with appropriate retention and access approval.

Exception handling acknowledges that incident evidence is often incomplete or contradictory. A gap discovered in triage or containment enters a dedicated evidence-exception path instead of being silently noted at closure. Missing, conflicting, or inaccessible records receive recovery actions and a documented limitation. Recovered evidence returns to control validation so the conclusion is tested against the improved record. If the gap is fundamental, the response must be reconstructed from available sources and returned to triage. Remediation regression sends the case back to containment; failed validation sends it back to remediation. Even a prepared audit package can be reopened if a packaging gap reveals that its conclusion is not adequately supported.

These controls matter because an incident can expose both an operational failure and a failure of the control environment. Preserving provenance, approvals, test results, and known limitations allows management, regulators, customers, and auditors to distinguish fact from assumption. It also reduces reliance on memories or manually reconstructed timelines and ensures that technical recovery is not mistaken for demonstrated control effectiveness.

Layer 1 — Incident evidence lifecycle

This layer shows the complete evidentiary outcome from detection through triage, containment, remediation, validation, and audit-ready closure. It is designed for incident governance, compliance leadership, and auditors assessing whether response and control conclusions are supportable. It intentionally omits individual commands, artifacts, test cases, and evidence-owner assignments.

Layer 2 — Response evidence operations

This layer presents the coordinated response and evidence work: preserve, triage, contain, remediate, validate, package, and resolve evidence exceptions. It includes the important loops for record gaps, remediation regression, validation failure, evidence recovery, reconstruction, and package deficiencies. It excludes tool-specific response procedures, notification deadlines, and the precise audit workpaper format.

Layer 3 — Evidence checks and actions

This layer covers the concrete records and checks inside each stage: register alerts and control context, preserve logs, assess scope and obligations, assign owners, record commands and approvals, link corrective changes to requirements, test restored and compensating controls, reconcile evidence, document missing records, assemble artifact lineage, and approve retention and conclusions. It supports procedure, evidence-schema, and automation design while intentionally not specifying a security platform, incident taxonomy, forensic technique, regulatory regime, or retention duration.
Open interactive model
SMPrivileged access recertification

This example represents a periodic recertification of administrator, elevated, and other high-impact access. The objective is not merely to collect attestations. It is to establish a complete review population, connect accounts to accountable identities and role sources, obtain informed decisions from business or system owners, execute required removals, and prove that approved decisions match effective access at the end of the review period.

The standard path begins by defining the systems, privileged roles, review period, policy criteria, and accountable owners. Entitlements are collected from directories and target platforms, then reconciled to people, service identities, and authoritative role records. Owners receive enough context to make a meaningful retain, modify, or revoke decision, including stated business need and recent-use evidence. Revocations and privilege reductions are issued through controlled change requests and verified across dependent systems. Retained and remediated access converges in control reconciliation, where recorded decisions are compared with actual access. Certification occurs only when the review population, decisions, and remediation are complete and the evidence package can be sealed.

The exception routes address common access-governance weaknesses. An inventory gap returns to scope because an incomplete population cannot support certification. Orphaned accounts, disputed ownership, emergency access, or decisions that cannot be completed enter an access-exception process with compensating controls and expiry. Failed removals also become exceptions rather than disappearing into an operations queue. Insufficient exception evidence returns to the owner decision. Residual access found during reconciliation reopens removal, ensuring that a closed ticket is not mistaken for an effective revocation.

These controls matter because privileged access can bypass preventive controls, alter evidence, and materially affect systems or data. A well-designed recertification demonstrates completeness, informed accountability, least privilege, timely remediation, and a defensible treatment of exceptions. It also distinguishes access that was approved on paper from access that remained technically active.

Layer 1 — Access recertification lifecycle

This layer shows the control from scoped review to certified conclusion, with remediation and exceptions visible as governed outcomes. It is aimed at control owners, risk committees, and auditors deciding whether the periodic review operated effectively. It intentionally omits connector behavior, account-level evidence, owner prompts, and individual access-change tasks.

Layer 2 — Privileged access review operations

This layer presents the compliance work queues: scoping, inventory collection, owner decision, removal execution, exception handling, reconciliation, and certification. It includes loops for population gaps, disputed access, failed revocation, inadequate evidence, and residual privilege. It excludes platform-specific entitlement models, campaign tooling, and detailed approval matrices.

Layer 3 — Control checks and actions

This layer identifies the concrete tests and records needed to operate the control: select systems and roles, identify owners, collect entitlements, reconcile identities, present business need and usage, capture decisions, issue least-privilege changes, verify dependent systems, set compensating controls and expiry, compare decisions with effective access, and seal evidence. It supports procedure and automation design while intentionally not prescribing an identity-governance product, directory schema, policy frequency, or organization-specific role catalogue.
Open interactive model
SMThird-party compliance oversight

This example represents risk-based oversight of a vendor or other third party from proposed engagement through governed service, remediation, and exit. It recognizes that due diligence is not a one-time questionnaire. Compliance obligations must be translated into contract controls, monitored while the service operates, revisited when risk changes, and closed with evidence that access, assets, data, and residual obligations were handled appropriately.

The ordinary path starts by classifying the service, data handled, jurisdictions, subcontracting exposure, and accountable internal owners. Due diligence collects and assesses evidence such as beneficial ownership, sanctions screening, security controls, conduct indicators, licenses, and assurance reports. Requirements that pass assessment are converted into enforceable agreement terms covering control performance, notification, assurance, audit rights, and cooperation. The service then enters ongoing monitoring, where current attestations, performance indicators, adverse events, and changes in obligations are reviewed. A planned exit ends service access, recovers managed assets, and retains closure approval along with any surviving confidentiality, retention, or regulatory duties.

The exception paths avoid the false choice between unconditional approval and immediate termination. A due-diligence gap or missing contract control enters risk exception, where the unmet requirement, exposure, compensating controls, accountable approver, and expiry are recorded. An approved exception permits monitored operation; an exception that needs stronger controls moves into remediation. Monitoring findings also trigger a corrective-action plan with owners and dates. Completed actions return to monitoring only after evidence is verified. Failed remediation routes to exit, making termination a defined control outcome rather than an improvised response. Any later re-engagement begins again with current scope instead of inheriting stale assurance.

These controls matter because the organization remains accountable for many obligations performed through third parties. A traceable lifecycle helps compliance, procurement, information security, legal, and business owners distinguish inherent risk, contractual commitments, operating evidence, accepted residual risk, and unresolved control failure. It also prevents expired exceptions or old attestations from being treated as permanent approval.

Layer 1 — Third-party oversight lifecycle

This layer shows the engagement’s governance outcome from initial scope to monitored service or controlled exit. It is useful for accountable executives, risk owners, and oversight committees reviewing whether the third party remains within appetite. It intentionally omits individual questionnaire responses, contract clauses, monitoring metrics, and remediation tasks.

Layer 2 — Vendor compliance operations

This layer presents the cross-functional operating stages: scope, due diligence, contract controls, monitoring, remediation, exception management, and exit. It makes the decision routes for evidence gaps, contract gaps, adverse findings, accepted exceptions, failed remediation, and re-engagement explicit. It excludes jurisdiction-specific tests, sourcing workflow details, and the exact roles in a firm’s approval authority.

Layer 3 — Oversight checks and actions

This layer describes the concrete activities: classify service and data exposure, assign obligations and owners, collect ownership and control evidence, assess sanctions and conduct indicators, draft assurance and notification terms, review current attestations, define corrective actions, verify closure evidence, document compensating controls and expiry, revoke access, and recover assets. It supports control mapping and procedure design while deliberately remaining neutral about vendor tiering methodology, contract template, screening provider, assurance framework, and monitoring platform.
Open interactive model
Explore patternsReview product applications

Cabinet index

Explore Formal Foundry

Search the archive

Find a page

Type to search the published content.