×

Legal

Challenges

  • Legal work spans complex, evolving rules across jurisdictions and documents.
  • Manual review is slow, inconsistent, and prone to missed dependencies.
  • Obligations and deadlines are difficult to trace through changing matters.
  • Policy changes create uncertainty for established compliance decisions.

Problems We Solve

  • Formal Rule Representation Encode definitions, conditions, and exceptions precisely.
  • Obligation Checking Track duties, triggers, deadlines, and required evidence.
  • Policy Simulation Model outcomes before a rule or interpretation changes.
  • Consistency Validation Surface conflicts, gaps, and ambiguous dependencies.
  • Explainable Recommendations Present traceable guidance with its supporting rationale.

Domain portfolio

Application patterns

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

The Legal domain concerns definitions, jurisdiction, obligations, deadlines, exceptions, and dependencies across matters and documents. These applications turn a lawyer’s proposed rule statement into a setup-scoped, checked proposition and deterministic readback. They support obligation checking, change analysis, consistency review, and traceability; they do not determine governing law, resolve facts, or replace responsible counsel.
01 Contract obligation and notice-control workbench Explore pattern

System/use case

A contract operations workbench helps in-house counsel and contract managers express recurring duties, conditions precedent, notice requirements, cure paths, and renewal or termination windows for an executed agreement portfolio. The checked statements become reviewable control assertions attached to a clause and contract version, rather than free-floating summaries.

Operational setting

The system serves procurement, sales, legal operations, and matter counsel after execution. Inputs include approved agreement text, defined terms, party roles, amendment lineage, events, notices, and evidence links. The matter context identifies the applicable agreement, amendments, contractual role, and time convention; the tool does not infer which instrument controls.

Decision/claim boundary

The bounded claim is that a candidate proposition is well formed in an approved contract-obligations setup—for example, that a triggering event plus a notice condition entails a review duty. It is not a finding that the trigger occurred, notice was effective, a deadline was computed correctly, a clause is enforceable, or a remedy is available. Counsel remains the authority on interpretation, privilege, waiver, materiality, and governing law.

Candidate checked statements

Illustrative controlled-English propositions for a future setup could include:

  • “For every covered service interruption, if timely notice is recorded, the supplier has a cure obligation.”
  • “If the cure period expires and the breach remains unresolved, the matter is eligible for termination review.”
  • “Every renewal decision must be approved before the applicable notice deadline.”

These are candidate formulations, not statements that the current readback vocabulary already implements or that the underlying contract facts are true.

Example architecture

An agreement repository feeds versioned provisions, terms, dates, and party roles into a matter-scoped rule registry. Contract-lifecycle and records services supply events and evidence. Counsel selects the instruments and audited setup. FF Scribe proposes only from that vocabulary, checks the proposition in Agda, and stores the type, readbacks, sources, and counsel’s disposition in a review record. Automation may consume only propositions separately approved for operational use. Privileged material remains behind legal-system access controls.

Where verified readback fits

A lawyer or contract manager states the intended control in natural language. The model maps it to one setup-scoped proposition, not a contract interpretation in unrestricted code. Agda checks the candidate’s syntax and type against the curated vocabulary. If the checked type is supported by the partial readback translation, the finite audited family renders it deterministically; unsupported structure fails visibly and no prose is guessed. The practitioner compares a successful reading with the provision and matter intent, then explicitly accepts it or provides feedback. Type correctness establishes formal well-formedness only; practitioner acceptance confirms intended meaning, not legal validity or factual satisfaction.

Potential benefits

The workbench can reduce inconsistent clause summaries, clarify triggers and dependent duties, and expose missing assumptions before workflow activation. A versioned chain from clause to accepted readback improves handoffs, renewal-control testing, remediation, and auditability. Reviewers can compare controls without trusting generated prose.

Limits/adoption considerations

Contract language is contextual and often open textured. Setups need clause-family vocabularies, version governance, and jurisdiction-aware counsel review. Date arithmetic, amendment precedence, evidence authenticity, and event detection require separate validation. Production also requires matter authorization, privilege controls, segregation of duties, retention, and withdrawal of superseded propositions.
02 Regulatory applicability and obligation register Explore pattern

System/use case

A regulatory applicability workbench supports legal and compliance teams documenting why a business unit, activity, product, or facility is considered within or outside a defined obligation set. It turns counsel-approved applicability logic into reviewable propositions linked to definitions, thresholds, exceptions, and evidence expectations.

Operational setting

The application sits alongside a regulatory inventory and GRC platform. Inputs include rule versions, jurisdiction and entity profiles, licensed activities, classifications, control ownership, memoranda, and change notices. A policy owner maintains control mappings; counsel approves the source hierarchy and interpretation for each setup.

Decision/claim boundary

The checked proposition may express an implication among curated concepts, such as covered activity, jurisdictional scope, exemption, and reporting duty. It does not establish that a regulator would adopt the same construction, that source material is complete or current, that an entity actually meets a threshold, or that compliance has occurred. Conflicts of law, pre-emption, interpretive uncertainty, and enforcement discretion remain outside the compiler boundary and must be recorded by counsel.

Candidate checked statements

Illustrative candidates include:

  • “For every entity, if the entity conducts a covered activity in the selected jurisdiction and no approved exclusion applies, the entity has an assessment obligation.”
  • “If a reporting obligation applies and the required evidence is incomplete, the filing control is not ready for closure.”
  • “Every applicable obligation must have an accountable control owner.”

Example architecture

A legal-content pipeline preserves source snapshots and version metadata without promoting extracted text to authoritative rules. Entity masters provide normalized facts; a registry holds counsel-curated predicates. The workbench invokes FF Scribe and links accepted readbacks to the obligation register. A separate engine may evaluate approved propositions against verified facts, while humans handle ambiguity and exceptions. Provenance, setup version, compiler result, readback ID, and counsel acceptance preserve the decision boundary.

Where verified readback fits

Counsel or an authorized policy owner describes the intended applicability relationship. The model proposes a type using only the selected regulatory setup. Agda verifies that its binders, predicates, and implications compose correctly. The partial readback stage then either presents a supported checked structure through its deterministic family, including available evidence-oriented variants, or reports that the structure is unsupported. The legal reviewer accepts a successful reading or submits corrective feedback. This loop confirms neither the truth of entity data nor the authoritative meaning of the law; it confirms only type correctness followed by explicit human agreement about the formalized statement.

Potential benefits

Teams gain a more consistent obligation register and clearer traceability to controls. The explicit structure can help reviewers notice omitted exceptions or contradictions; it does not detect them automatically. Versioned propositions show which accepted claims depend on a changed definition. The record separates source selection, interpretation, formalization, fact evaluation, and control attestation.

Limits/adoption considerations

Rule ingestion, citation currency, and entity data quality remain independent risks. Organizations need counsel-approved taxonomies, effective-date handling, explicit uncertainty, and escalation rather than forced binary answers. Vocabulary changes require readback audit. Public deployment also requires isolation, authentication, durable audit storage, and sensitive-data controls.
03 Litigation elements and procedural-readiness assistant Explore pattern

System/use case

A matter-support assistant helps litigation teams articulate claim or defense elements, prerequisite showings, preservation duties, and procedural readiness conditions. Its purpose is to quality-check the structure of counsel’s litigation theory and task gates, not to predict outcomes or automate advocacy.

Operational setting

The tool operates within matter-management and evidence-review systems. Counsel selects a setup derived from an approved elements memorandum or playbook. Facts, allegations, evidence references, orders, service events, and dates remain in their systems of record. Attorneys control assumptions, disputed issues, and privilege.

Decision/claim boundary

A candidate can say that a set of premises entails an internal readiness classification or that every asserted claim requires a named element. Type checking does not prove any element, authenticate evidence, calculate a limitations period, satisfy a burden of proof, or establish that a filing is procedurally valid. The responsible lawyer owns the legal theory, source authority, factual characterization, strategic judgment, and final filing decision.

Candidate checked statements

Possible controlled-English candidates are:

  • “For every asserted claim, if a required element lacks a linked evidentiary basis, the claim requires attorney review.”
  • “If service is confirmed and the response deadline is approved, the response task has a scheduling obligation.”
  • “Every dispositive-motion recommendation requires an approved issue statement and a supporting record reference.”

Example architecture

The matter platform supplies permissions and task state; docketing supplies lawyer-approved dates; document review supplies evidence identifiers. A versioned issue graph holds counsel-authored elements. FF Scribe checks a proposed statement and produces deterministic readbacks linked to—not substituted for—the graph and deadline system. Filing, waiver, preservation release, and client communication require human approval. Session logs are governed as potentially privileged work product.

Where verified readback fits

The attorney describes the desired issue or readiness rule in ordinary professional language. A model produces a single setup-constrained proposition or asks for clarification. Agda accepts or rejects its formal construction; bounded repair can address compiler diagnostics. A well-typed structure within the configured readback slice yields the finite deterministic family, while unsupported translation fails visibly. The attorney compares a successful reading with the intended theory and provides explicit acceptance or feedback. Passing the type checker is not proof completion, and acceptance is not an adjudication of law or fact; it records only that counsel recognizes the checked statement as the intended internal proposition.

Potential benefits

The assistant can expose hidden assumptions, improve issue-outline consistency, and link an internal rule to counsel-approved wording. It may reduce missed dependencies, support case reviews, and distinguish absent evidence from a negative finding. Litigators need not read Agda.

Limits/adoption considerations

Adversarial facts, evolving theories, local practice, and tactics resist rigid encoding. Vocabularies must be narrow and matter governed; disputed propositions need explicit status. Deadline systems require independent validation and attorney review. Organizations need privilege labeling, supervisory controls, conflict screening, audit access, and setup-supersession procedures.
04 Legal change-impact and interpretation comparison service Explore pattern

System/use case

A legal change-impact service lets counsel compare proposed interpretations or rule versions before changing established guidance, controls, forms, or decision procedures. It represents dependencies among defined terms, scope conditions, exceptions, obligations, and recommendations so affected propositions can be reviewed deliberately.

Operational setting

The service supports horizon scanning and policy governance using source snapshots, counsel-authored change notes, accepted propositions, affected processes, and representative scenarios. It can compare counsel-curated setups but does not decide which text or interpretation controls.

Decision/claim boundary

The formal claim is limited to the structural consequences expressed by a selected version—for example, that a newly defined covered category entails an additional assessment step. A successful check does not prove the amendment’s legal effect, forecast enforcement, validate a scenario’s facts, or show that all downstream impacts were found. Counsel approves the authoritative source, effective period, interpretive assumptions, and operational disposition.

Candidate checked statements

Illustrative comparison candidates include:

  • “Under the proposed rule version, every newly covered service has a documentation obligation.”
  • “If the revised definition applies to an existing matter, that matter requires applicability reassessment.”
  • “If two approved rules assign incompatible dispositions to the same classified case, the case requires legal escalation.”

Example architecture

A source store and dependency graph map rules to accepted propositions, controls, templates, and requirements. Counsel curates baseline and proposed setups. A runner submits representative statements to FF Scribe and records compiler outcomes and readback IDs. A diff service compares structures and downstream references; a dashboard assigns impacts. Approved interpretations pass through existing change gates, with old setups retained for reproducibility.

Where verified readback fits

An authorized lawyer states an expected consequence for a selected baseline or proposed setup. The model translates it into that setup’s finite vocabulary, and Agda checks the proposition’s type. If its structure is supported, the audited readback family deterministically exposes quantified entities, premises, and conclusion; otherwise translation stops visibly. The lawyer accepts a successful reading or supplies feedback, producing a versioned, reviewable proposition for comparison. Type correctness is distinct from legal truth; a checked statement may be incomplete, based on an unauthorized interpretation, or inconsistent with user intent until professional review is complete. Nor does the workflow construct a proof that the conclusion follows from real-world facts.

Potential benefits

The service can reveal decisions relying on changed definitions, compare interpretations in stable language, and prioritize widely connected controls. It preserves why guidance changed and surfaces conflicts before implementation. Reviewers see formal structure and lawyer-approved readback, not opaque generated recommendations.

Limits/adoption considerations

Completeness depends on the dependency inventory and the quality of counsel’s setups. Temporal rules, transitional provisions, cross-jurisdiction interactions, and non-textual authorities may require specialized modeling or remain unsupported. The service needs rigorous source provenance, semantic versioning, dual review for high-impact changes, deprecation rules, and monitoring for stale accepted statements. Operational impact analysis and authoritative legal judgment remain human-led activities.

Applicability frame

MLTTDB is most plausible here as a controlled boundary between a lawyer-owned formal model and changing, reviewable source-language records. Row types and :T: table declarations remain in Agda, Lean, or Rocq source; the SQLite term store retains ordered records, UUIDs, projections, language metadata, and table metadata. The proof assistant—not the store—performs semantic checking, whether invoked by a project pipeline or orchestrated by the store. Agda currently supports finite UUID lookup between eligible stored rows; Lean and Rocq preprocessors validate generated definitions but do not provide that lookup. Matter intake, document extraction, authority research, identity and access, source-system reconciliation, workflow, runtime controls, provenance, and formalization approval are separate production responsibilities.

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 legal review.

01 Contract obligation lifecycle assurance Explore pattern

Operational context

A commercial legal-operations team maintains a portfolio of negotiated supply, outsourcing, and services agreements. Obligations arise from events such as an effective date, acceptance, renewal notice, service failure, or termination. The contract repository holds executed documents, while matter owners need a dependable view of which normalized obligation templates, trigger categories, notice routes, and evidence requirements can coexist. The hard problem is not merely extracting clauses: it is preventing a reviewed obligation catalogue from acquiring impossible dates, incompatible trigger/actor combinations, or dangling references as lawyers refine it.

Why MLTTDB fits

Counsel can define the admissible vocabulary and invariants as proof-assistant types: a notice obligation must name an obligated party, recipient role, trigger, period convention, and permitted delivery channel; a cure right can only refer to an earlier breach-notice pattern. Analysts can then edit ordered, UUID-addressed source terms without weakening those types. Agda finite lookup is useful when a reviewed obligation row refers to a previously declared trigger or notice pattern. If the organization standardizes on Lean or Rocq, the model should instead use generated identifiers or self-contained rows because their current preprocessors do not implement finite table lookup.

Example architecture

executed contracts -> extraction/reconciliation -> lawyer review workbench
                                                  |
proof model repo -> CI ----> MLTTDB SQLite <-------+ curated typed records
                       fetch/orchestrate verify -> Agda/Lean/Rocq -> evidence bundle

The repository owns types, declarations, contract-family modules, and propositions. An external extraction service proposes clause spans and source coordinates; the workbench requires a lawyer to accept or correct them and writes only normalized, source-language records to MLTTDB. Verification runs against a pinned model revision. A separate obligation-management platform consumes only approved exports and executes reminders, assignments, and escalations.

Representative typed artifacts

The model could declare triggerPatterns :T: TriggerPattern, noticePatterns :T: NoticePattern, and obligationTemplates :T: ObligationTemplate. Types distinguish calendar from business-day periods, one-off from recurring duties, and conditions precedent from post-trigger duties. A proposition such as wellFormedObligation checks that the selected action is available to the actor role, required evidence matches the action, and any referenced notice or cure pattern is compatible. External metadata links each UUID to agreement, clause span, reviewer, and approval record; those links are not proof of the contract text’s truth.

Checks and evidence

CI exercises schema mode before analysts receive a new model. Data-mode verification then checks every current record and emits proof-assistant diagnostics and generated source where applicable. A release job records the model commit, database snapshot identifier, ordered UUID list, verification output, tool versions, and legal approvals in an external evidence repository. Negative fixtures cover unknown references, invalid party roles, contradictory duration conventions, and cycles. Sampling compares normalized terms back to executed clauses.

Potential benefits

The team gains earlier detection of catalogue inconsistencies, a reviewable separation between legal semantics and portfolio data, and repeatable regression checks when templates change. UUIDs support stable discussion of rows, while ordering makes review exports deterministic. The evidence bundle can show exactly what was checked and under which model without claiming that the software interpreted the agreement conclusively.

Deployment boundary

MLTTDB does not extract clauses, determine contractual meaning, establish that an event occurred, send notices, calculate authoritative deadlines, or enforce an obligation. The contract repository and approval system remain systems of record. Runtime reminders must fail safely and expose their source assumptions. Privilege, confidentiality, retention, legal hold, access segregation, and professional review require controls outside MLTTDB; a qualified lawyer approves every template and matter-specific conclusion.
02 Litigation and regulatory deadline rule regression Explore pattern

Operational context

A docketing function supports disputes and regulated submissions across multiple forums. Deadline rules combine event type, service method, counting convention, excluded days, extensions, and discretionary orders. The organization already has a docketing engine and authoritative calendars, but changes to its rule packs are difficult to review: a revised definition may alter thousands of scenarios, and a malformed rule can silently omit a required input. The proposed system is a pre-release assurance environment for rule packs, not the live calendar.

Why MLTTDB fits

Formal row types can make each rule explicit about forum profile, triggering event, period, counting method, adjustment policy, and authority reference. Scenario tables can encode reviewed inputs and expected structural outcomes. An external rule-pack compiler can materialize a reconciled DeadlineRuleManifest aggregate term. Proofs can then establish properties such as “a computed due date is not earlier than its trigger” under the modeled calendar assumptions, or that every mandatory event class enumerated by the manifest maps to exactly one applicable rule in a selected profile. Ordered records make regression suites stable, and UUIDs give reviewers durable handles across revisions.

Example architecture

authority monitoring -> counsel-authored rule proposal -> rule-model branch
authoritative calendars -> scenario builder -> MLTTDB scenario/rule records
model and records -> proof-assistant validation -> evidence review -> release gate

Legal researchers monitor authorities in an external service. Counsel translates approved changes into a model branch and curated records. A calendar adapter snapshots the holidays and closure assumptions used for testing. Each regression scenario carries a counsel-reviewed declared DeadlineResult and witness under the selected rule-pack model. MLTTDB supplies those rows to the proof-assistant validation path. A release-gate service compares the checked declarations with the previous approved pack and routes material differences to docketing counsel before a separate deployment mechanism updates the operational engine; generic data-mode output is not treated as a computed calendar-result API.

Representative typed artifacts

Tables might include forumProfiles :T: ForumProfile, deadlineRules :T: DeadlineRule, and regressionScenarios :T: DeadlineScenario. DeadlineRule can require an effective interval, event kind, duration, day-count basis, service adjustment, and precedence class. DeadlineScenario includes the reviewed inputs, a declared DeadlineResult, and a witness that the selected model relates those inputs to that result. The model can represent an explicit AuthorityRef as a typed identifier with review status, while leaving the authoritative text in the legal research system. In Agda, a scenario could refer by UUID to an earlier rule or forum row; Lean/Rocq deployments should materialize an equivalent generated definition structure without assuming that lookup feature.

Checks and evidence

Schema checks reject declarations that no longer elaborate. Data checks reject missing fields, malformed rule alternatives, illegal references, and declared-result witnesses that fail. The regression harness compares checked declarations for boundary scenarios around excluded days, service adjustments, effective-date transitions, and overriding orders. Review output should include old/new declared results, changed model and row UUIDs, calendar snapshot identity, proof-assistant diagnostics, comparator version, and explicit counsel disposition. Independent reconciliation against a sample from the production docketing engine detects translation drift.

Potential benefits

Rule-pack changes become inspectable before they reach live matters. Reviewers see which assumptions and scenarios changed rather than receiving an opaque code diff. Typed cases reduce structurally incomplete rules, and propositions catch contradictions that ordinary field validation misses. The organization can retain reproducible review evidence for internal quality assurance while keeping its existing docket workflow and escalation practices.

Deployment boundary

MLTTDB does not research authorities, decide which rule controls, know whether service was effective, maintain an authoritative court calendar, docket a matter, or guarantee a deadline. Court orders and professional judgment can override modeled defaults. The live system needs dual review, clock and calendar governance, urgent exception handling, access controls, monitoring, and tested fallback procedures. No deadline is released or relied upon without qualified counsel and docketing review.
03 Data-processing and transfer clause pre-decision review Explore pattern

Operational context

Privacy counsel reviews data-processing agreements, security schedules, subprocessor terms, and cross-border transfer provisions during vendor onboarding. A questionnaire and contract-analysis service can identify candidate facts, but the review team must determine whether the proposed clause set contains required concepts for the intended processing profile and whether negotiated deviations are internally coherent. Terminology varies across templates and jurisdictions, so the architecture focuses on organization-approved control patterns rather than asserting a universal legal test.

Why MLTTDB fits

A proof-assistant model can distinguish roles, processing purposes, data categories, transfer situations, safeguard families, audit commitments, deletion duties, and exception approvals. MLTTDB lets analysts maintain proposed agreement profiles and clause-pattern selections as typed source terms while the semantic checker enforces relationships defined by privacy counsel. For example, the model can reject a profile that selects a transfer mechanism incompatible with its modeled party roles, or requires a supplementary-control assessment but supplies no reviewed assessment reference.

Example architecture

vendor intake and contract -> extraction/classification -> privacy review UI
approved clause library ----> formal-model mapping -----> MLTTDB records
model repo and records -> proof-assistant verification -> approval workflow

The intake platform owns vendor identity, processing facts, attachments, and source text. Extraction proposes mappings with confidence and text spans. A privacy professional confirms those facts and chooses approved clause patterns in the review UI. An adapter renders the reviewed selections as source-language records. Store-orchestrated or CI verification invokes Agda, Lean, or Rocq; a findings service translates checker output into reviewer-facing language and sends dispositions to the existing third-party risk workflow.

Representative typed artifacts

Possible declarations include processingProfiles :T: ProcessingProfile, clauseAssessments :T: ClauseAssessment, and deviationApprovals :T: DeviationApproval. Sum types prevent conflating controller/processor role claims with transfer-role claims. A ClauseAssessment carries a clause-family identifier, applicability rationale category, reviewer-confirmed source span reference, and disposition. A reconciled ClauseCoverageManifest aggregate term enumerates counsel-designated categories, accepted patterns, deviations, and assessment UUIDs; proof obligations can require every category represented there to be satisfied by an accepted pattern or an authorized deviation. Agda lookup can connect an assessment to earlier approved pattern rows; the other current backends need self-contained or generated references.

Checks and evidence

Validation checks the reconciled manifest’s coverage of counsel-designated requirement categories, typed compatibility of role and safeguard selections, effective intervals for approved patterns, and absence of reference cycles in the represented dependency graph. Scenario suites model representative vendor arrangements and negotiated combinations, including negative cases for missing subprocessors, incompatible deletion commitments, and lapsed deviations. Evidence should pair the checker result with the formal-model revision, ordered record snapshot, manifest reconciliation, confirmed clause spans, extraction-versus-review changes, and named legal approval. Source text remains independently retrievable from the contract system.

Potential benefits

The approach can reduce inconsistent application of an internal clause playbook, expose missing review inputs before signature, and make deviations easier to compare across vendors. Formal types turn ambiguous dropdown combinations into explicit modeling questions. Repeatable scenarios help privacy teams understand the operational effect of playbook revisions, and retained evidence distinguishes machine-proposed mappings from lawyer-confirmed conclusions.

Deployment boundary

MLTTDB does not classify parties conclusively, establish where processing occurs, determine legal adequacy, monitor legal change, draft negotiated text, or authorize a transfer. Extraction confidence is not evidence of a legal fact. Data mapping, vendor identity, document custody, access, privilege, retention, and workflow remain external. Counsel must approve the formal categories, jurisdiction-specific overlays, exceptions, and every agreement disposition before contracting or data movement proceeds.
04 Insurance-claims coverage and denial-reason packet assurance Explore pattern

Operational context

An insurer’s coverage unit and legal function review complex property, casualty, or specialty claims before issuing a reservation-of-rights, partial coverage, or denial communication. The claim system contains loss notices, investigation material, adjuster findings, and payment activity; the policy administration system holds declarations, forms, endorsements, and effective periods. The assurance problem is whether a proposed coverage-position packet uses the reviewed policy-form set, distinguishes established findings from open questions, and connects each proposed reason to the applicable insuring agreement, condition, exclusion, or endorsement. It is not an automated coverage determination.

Why MLTTDB fits

Coverage counsel can define typed abstractions for policy-form profiles, coverage provisions, endorsements, exclusions, conditions, confirmed findings, unresolved issues, position categories, communication reasons, and complaint or appeal routes. A packet term can carry the adjuster’s reviewed findings and the proposed position together with witnesses that each reason is permitted by the selected internal model. Type distinctions can prevent an allegation or unverified investigation item from being used as a confirmed predicate. Separating the legal model from case packets also permits synthetic regression when an approved form interpretation or reason template changes.

Example architecture

policy administration + claims/evidence system
                  |
      adjuster-confirmed findings and form reconciliation
                  v
       MLTTDB typed coverage-position packet
                  |
       Agda/Lean/Rocq validation status and diagnostics
                  v
 coverage counsel review -> correspondence workflow -> claim file

Policy administration and claims platforms remain the systems of record. A projection service resolves the in-force form and endorsement identifiers, preserves source references, and reports reconciliation gaps. The term store holds a minimal, preferably pseudonymized packet under a pinned legal-model revision. The proof assistant validates its typed declarations; a project-owned adapter maps native diagnostics and UUIDs into the counsel workbench. Authorized reviewers record their interpretation and approve any communication through the existing claims workflow.

Representative typed artifacts

Declarations could include formProfiles :T: PolicyFormProfile, coveragePackets :T: CoveragePositionPacket, and communicationReasons :T: CoverageReason. A PolicyFormProfile identifies the reviewed declarations, base form, endorsements, and effective interval without storing the authoritative documents. CoveragePositionPacket separates reported assertions, investigator-confirmed findings, disputed facts, unresolved coverage questions, proposed disposition, and escalation state. A reason artifact relates one reviewed provision and finding category to a proposed explanation; it does not assert that the provision controls as a matter of law. Agda lookup may connect a packet to an earlier form-profile row, while a portable design uses self-contained or ordinarily generated associations.

Checks and evidence

Validation can reject an unknown or out-of-period form profile, a reason that is not permitted for the declared position category, a cited endorsement absent from the reviewed form set, an unresolved question represented as a confirmed finding, or a proposed communication without the modeled review or complaint route. Synthetic regression packets should cover conflicting endorsements, multiple causes of loss, late or incomplete information, reservation states, partial coverage, and reason-template changes. External evidence should bind the policy and claim revisions, projection reconciliation, formalization commit, ordered row UUIDs, checker diagnostics, counsel comments, approval record, and final correspondence hash.

Potential benefits

Coverage reviews can become more consistent about form selection, finding status, reason provenance, and escalation. Typed packets can expose structural gaps before correspondence is issued, while stable UUIDs make legal comments and remediation traceable. Regression cases show which reviewed packets no longer validate after a model or template change without presenting that result as a substantive coverage conclusion.

Deployment boundary

MLTTDB does not read a policy conclusively, decide which provision controls, assess credibility or causation, determine coverage or bad-faith exposure, value a loss, authorize payment, draft legal advice, issue correspondence, or resolve a complaint or appeal. Privilege, confidentiality, document custody, fair-claims handling, jurisdiction-specific duties, deadlines, access control, and human authority remain external. Qualified coverage professionals and counsel must approve the form mapping, formal model, case-specific interpretation, and every consequential communication.

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

Public-Benefit Adjudication and Appeal

About this workflow

This example represents a public-benefit case from application through an appealable, reasoned determination. It is deliberately program-neutral: the controlling definitions, thresholds, exclusions, filing rules, and review rights can be supplied for a particular benefit and jurisdiction. The model’s concern is procedural integrity—using the right rule version, building a complete record, explaining the result, and preserving a genuine route for review.

The ordinary case begins by recording the benefit sought, filing jurisdiction, application date, and applicant identity. Evidence review maps the submitted record to required categories, requests missing or stale material, and tracks response deadlines and authorized extensions. Once the record is sufficiently complete, eligibility determination applies the definitions and criteria effective for the case, considers thresholds, exclusions, and stated exceptions, and records the rule path for each finding. A separate decision review checks the proposed outcome, reasons, and citations before accountable approval. The issued notice communicates the outcome, reasons, effective date, and applicable appeal window. If no appeal is filed in time, the operative outcome is closed and retained.

The return paths protect both the claimant and the deciding authority. Invalid intake can be corrected without silently losing the original filing context. Missing evidence sends the matter back to evidence development. Inconsistent reasoning is remanded before a decision is issued. A timely appeal reopens contested findings and permits supplemental evidence; the reviewer may affirm, revise, or remand. A remand can return to evidence collection, while an appeal outcome is reissued with a renewed operative decision. These controls matter because eligibility is not merely a yes-or-no calculation: jurisdiction, effective dates, notice, deadlines, review authority, and an auditable explanation can determine whether a legally correct result was reached through a fair process.

Layer 1 — Adjudication stages

This layer shows the case-level progression used by program counsel, supervisors, and appeals staff: intake, evidence development, eligibility determination, decision review, issuance, appeal, and closure. It exposes remands and reopening paths without overwhelming the reader with individual documents. It intentionally excludes caseworker keystrokes and criterion calculations so procedural posture and decisional authority remain clear.

Layer 2 — Eligibility and appeal procedures

This layer expands each stage into the procedures that establish a defensible administrative record. It includes evidence-category mapping, deadline management, application of effective definitions, reason drafting, citation checking, accountable review, timeliness analysis, and reconsideration of contested findings. It is appropriate for policy manuals and quality assurance. It does not encode the substantive formula for any one benefit program.

Layer 3 — Caseworker actions

This layer identifies the concrete work items performed on a case: recording filing facts, issuing a request for evidence, documenting an extension, evaluating each criterion, checking rule versions, calculating the appeal window, and preserving notices and review history. It supports task assignment and audit reconstruction. Jurisdiction-specific forms, document templates, and system screen interactions are intentionally left to the implementing agency.
02

Multi-Jurisdiction Contract Obligations

About this workflow

This example models obligation management for a contract whose duties are distributed across the main agreement, schedules, amendments, and jurisdiction-specific overlays. It treats a contract as an active network of defined terms, triggering events, responsible parties, notice mechanics, deadlines, exceptions, and remedies—not as a static signed PDF.

The workflow starts by identifying the operative document set, incorporated materials, governing law, parties, and effective dates. Clause mapping normalizes defined terms, resolves document precedence, extracts conditions and exceptions, and assigns each obligation to a responsible party. Once activated, monitoring watches for events such as delivery milestones, renewals, consent requests, volume thresholds, or termination dates, then recalculates the relevant windows. A triggered obligation becomes due: the responsible party is notified, evidence of payment, delivery, consent, or notice is collected, and performance is tested for timeliness and contractual sufficiency. Satisfied performance returns the contract to active monitoring. At term, surviving duties and final notices are resolved before closure.

The machine also preserves the legal response when performance is incomplete or disputed. An incorrect document set returns to intake because downstream conclusions cannot safely rest on missing amendments. An unmet obligation moves into breach and cure, where the duty, available remedy, required notice, cure period, corrective action, and reservation of rights are tracked. A completed cure can restore monitoring; a disputed cure reopens the obligation for evaluation; an uncured material breach may close the relationship through the authorized termination path. These controls matter to contract managers and counsel because missed dependencies often arise from cross-references and changing dates, while an otherwise valid remedy can be lost through defective notice or failure to preserve rights.

Layer 1 — Contract lifecycle

This layer provides the portfolio and matter-level view: intake, clause mapping, active monitoring, performance due, breach and cure, and closure. It shows when the contract is merely being interpreted versus when a live duty or remedy is in play. It intentionally excludes clause-by-clause extraction details so counsel and contract owners can see the operative posture quickly.

Layer 2 — Obligation management procedures

This layer describes how the legal operations team turns text into controlled work. It includes normalizing definitions, applying precedence, associating duties with parties, monitoring triggers, calculating notice and renewal windows, evaluating evidence, issuing cure notices, and tracking reservations of rights. It is suitable for playbooks and workflow configuration. It excludes the wording of any particular negotiated clause.

Layer 3 — Clause-level actions

This layer exposes the individual actions used to support a conclusion: identify an incorporated schedule, map a defined term, record an exception, apply a jurisdictional overlay, notify an owner, collect proof of performance, and archive the evidence timeline. It enables review of exactly how an obligation was derived and handled. Document-specific citation coordinates, email templates, and repository APIs are intentionally implementation details beyond this example.
03

Regulatory Matter and Deadline Management

About this workflow

This example represents the controlled response to a regulator, supervisory authority, or other rule-bound legal request. It covers preservation and collection, privilege and responsiveness review, preparation of an approved response, filing, follow-up, remediation, and closure. The model is intentionally neutral about the authority so its procedures can be adapted to an information request, examination, notice, subpoena, or similar matter.

Opening the matter establishes the issuing authority, jurisdiction, request scope, and the deadlines for response, preservation, and internal escalation. Scoped holds and collection instructions then identify custodians and sources, track completeness, and escalate unavailable or altered records. Privilege review classifies responsive material, records the applicable privilege grounds, applies redactions or withholding, and produces the supporting privilege record. Response preparation maps each requested item to produced material or a reasoned explanation, addresses missing items and exceptions, and obtains responsible legal approval. Filing uses the required channel, confirms receipt, and tracks follow-up, correction, extension, and remediation dates until all obligations are fulfilled.

Several loops prevent a superficially complete response from becoming an unreliable filing. Privilege review can return an incomplete collection for additional records. Response preparation can reopen collection when an evidentiary gap appears. A missed deadline, rejected submission, or scope dispute enters a matter exception rather than being handled informally. The corrective path may seek an extension, repair and resubmit the filing, reopen substantive preparation, or escalate for accountable approval. Closure occurs only after final obligations and holds have been resolved and the record of decisions, productions, filings, and evidence is preserved. These controls matter because defensibility depends on chain of custody, consistent privilege treatment, timely action, approval, and proof of receipt as much as on the prose of the response.

Layer 1 — Matter lifecycle

This layer gives lead counsel and matter managers the procedural posture: opened, collecting, under privilege review, preparing a response, filed and monitored, in exception, or closed. It highlights rework and corrective paths alongside the normal progression. It intentionally suppresses document-level decisions so leadership can assess scope, deadline risk, and accountability at a glance.

Layer 2 — Response and filing procedures

This layer covers the repeatable legal operations procedures within each posture: calculating deadlines, issuing preservation instructions, reconciling custodians and sources, applying review protocols, preparing a privilege record, mapping requests to responses, obtaining approval, confirming receipt, and managing remediation. It supports matter plans and quality gates. It excludes the substantive legal position taken in a particular response.

Layer 3 — Document-level actions

This layer exposes the concrete handling steps for records and filing components: classify responsiveness, identify a privilege basis, redact or withhold, explain a missing item, route a draft for approval, submit through the prescribed channel, and record confirmation. It supports production audits and exception investigation. Review-platform commands, file formats, and authority-specific portal mechanics remain outside the generic model.
Interactive state machine

Workflow demo

Skip to content

Domains

Legal

Placeholder domain page for legal rules involving definitions, jurisdiction, and obligations.

  • definitions
  • jurisdiction
  • obligations

Problems we solve

Checked boundaries and evidence

  • Legal work spans complex, evolving rules across jurisdictions and documents.
  • Manual review is slow, inconsistent, and prone to missed dependencies.
  • Obligations and deadlines are difficult to trace through changing matters.
  • Policy changes create uncertainty for established compliance decisions.
Formal Rule Representation

Encode definitions, conditions, and exceptions precisely.

Obligation Checking

Track duties, triggers, deadlines, and required evidence.

Policy Simulation

Model outcomes before a rule or interpretation changes.

Consistency Validation

Surface conflicts, gaps, and ambiguous dependencies.

Explainable Recommendations

Present traceable guidance with its supporting rationale.

Application patterns

Imported product records

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

FF Scribe4 patterns
The Legal domain concerns definitions, jurisdiction, obligations, deadlines, exceptions, and dependencies across matters and documents. These applications turn a lawyer’s proposed rule statement into a setup-scoped, checked proposition and deterministic readback. They support obligation checking, change analysis, consistency review, and traceability; they do not determine governing law, resolve facts, or replace responsible counsel.
01Contract obligation and notice-control workbench

System/use case

A contract operations workbench helps in-house counsel and contract managers express recurring duties, conditions precedent, notice requirements, cure paths, and renewal or termination windows for an executed agreement portfolio. The checked statements become reviewable control assertions attached to a clause and contract version, rather than free-floating summaries.

Operational setting

The system serves procurement, sales, legal operations, and matter counsel after execution. Inputs include approved agreement text, defined terms, party roles, amendment lineage, events, notices, and evidence links. The matter context identifies the applicable agreement, amendments, contractual role, and time convention; the tool does not infer which instrument controls.

Decision/claim boundary

The bounded claim is that a candidate proposition is well formed in an approved contract-obligations setup—for example, that a triggering event plus a notice condition entails a review duty. It is not a finding that the trigger occurred, notice was effective, a deadline was computed correctly, a clause is enforceable, or a remedy is available. Counsel remains the authority on interpretation, privilege, waiver, materiality, and governing law.

Candidate checked statements

Illustrative controlled-English propositions for a future setup could include:

  • “For every covered service interruption, if timely notice is recorded, the supplier has a cure obligation.”
  • “If the cure period expires and the breach remains unresolved, the matter is eligible for termination review.”
  • “Every renewal decision must be approved before the applicable notice deadline.”

These are candidate formulations, not statements that the current readback vocabulary already implements or that the underlying contract facts are true.

Example architecture

An agreement repository feeds versioned provisions, terms, dates, and party roles into a matter-scoped rule registry. Contract-lifecycle and records services supply events and evidence. Counsel selects the instruments and audited setup. FF Scribe proposes only from that vocabulary, checks the proposition in Agda, and stores the type, readbacks, sources, and counsel’s disposition in a review record. Automation may consume only propositions separately approved for operational use. Privileged material remains behind legal-system access controls.

Where verified readback fits

A lawyer or contract manager states the intended control in natural language. The model maps it to one setup-scoped proposition, not a contract interpretation in unrestricted code. Agda checks the candidate’s syntax and type against the curated vocabulary. If the checked type is supported by the partial readback translation, the finite audited family renders it deterministically; unsupported structure fails visibly and no prose is guessed. The practitioner compares a successful reading with the provision and matter intent, then explicitly accepts it or provides feedback. Type correctness establishes formal well-formedness only; practitioner acceptance confirms intended meaning, not legal validity or factual satisfaction.

Potential benefits

The workbench can reduce inconsistent clause summaries, clarify triggers and dependent duties, and expose missing assumptions before workflow activation. A versioned chain from clause to accepted readback improves handoffs, renewal-control testing, remediation, and auditability. Reviewers can compare controls without trusting generated prose.

Limits/adoption considerations

Contract language is contextual and often open textured. Setups need clause-family vocabularies, version governance, and jurisdiction-aware counsel review. Date arithmetic, amendment precedence, evidence authenticity, and event detection require separate validation. Production also requires matter authorization, privilege controls, segregation of duties, retention, and withdrawal of superseded propositions.
02Regulatory applicability and obligation register

System/use case

A regulatory applicability workbench supports legal and compliance teams documenting why a business unit, activity, product, or facility is considered within or outside a defined obligation set. It turns counsel-approved applicability logic into reviewable propositions linked to definitions, thresholds, exceptions, and evidence expectations.

Operational setting

The application sits alongside a regulatory inventory and GRC platform. Inputs include rule versions, jurisdiction and entity profiles, licensed activities, classifications, control ownership, memoranda, and change notices. A policy owner maintains control mappings; counsel approves the source hierarchy and interpretation for each setup.

Decision/claim boundary

The checked proposition may express an implication among curated concepts, such as covered activity, jurisdictional scope, exemption, and reporting duty. It does not establish that a regulator would adopt the same construction, that source material is complete or current, that an entity actually meets a threshold, or that compliance has occurred. Conflicts of law, pre-emption, interpretive uncertainty, and enforcement discretion remain outside the compiler boundary and must be recorded by counsel.

Candidate checked statements

Illustrative candidates include:

  • “For every entity, if the entity conducts a covered activity in the selected jurisdiction and no approved exclusion applies, the entity has an assessment obligation.”
  • “If a reporting obligation applies and the required evidence is incomplete, the filing control is not ready for closure.”
  • “Every applicable obligation must have an accountable control owner.”

Example architecture

A legal-content pipeline preserves source snapshots and version metadata without promoting extracted text to authoritative rules. Entity masters provide normalized facts; a registry holds counsel-curated predicates. The workbench invokes FF Scribe and links accepted readbacks to the obligation register. A separate engine may evaluate approved propositions against verified facts, while humans handle ambiguity and exceptions. Provenance, setup version, compiler result, readback ID, and counsel acceptance preserve the decision boundary.

Where verified readback fits

Counsel or an authorized policy owner describes the intended applicability relationship. The model proposes a type using only the selected regulatory setup. Agda verifies that its binders, predicates, and implications compose correctly. The partial readback stage then either presents a supported checked structure through its deterministic family, including available evidence-oriented variants, or reports that the structure is unsupported. The legal reviewer accepts a successful reading or submits corrective feedback. This loop confirms neither the truth of entity data nor the authoritative meaning of the law; it confirms only type correctness followed by explicit human agreement about the formalized statement.

Potential benefits

Teams gain a more consistent obligation register and clearer traceability to controls. The explicit structure can help reviewers notice omitted exceptions or contradictions; it does not detect them automatically. Versioned propositions show which accepted claims depend on a changed definition. The record separates source selection, interpretation, formalization, fact evaluation, and control attestation.

Limits/adoption considerations

Rule ingestion, citation currency, and entity data quality remain independent risks. Organizations need counsel-approved taxonomies, effective-date handling, explicit uncertainty, and escalation rather than forced binary answers. Vocabulary changes require readback audit. Public deployment also requires isolation, authentication, durable audit storage, and sensitive-data controls.
03Litigation elements and procedural-readiness assistant

System/use case

A matter-support assistant helps litigation teams articulate claim or defense elements, prerequisite showings, preservation duties, and procedural readiness conditions. Its purpose is to quality-check the structure of counsel’s litigation theory and task gates, not to predict outcomes or automate advocacy.

Operational setting

The tool operates within matter-management and evidence-review systems. Counsel selects a setup derived from an approved elements memorandum or playbook. Facts, allegations, evidence references, orders, service events, and dates remain in their systems of record. Attorneys control assumptions, disputed issues, and privilege.

Decision/claim boundary

A candidate can say that a set of premises entails an internal readiness classification or that every asserted claim requires a named element. Type checking does not prove any element, authenticate evidence, calculate a limitations period, satisfy a burden of proof, or establish that a filing is procedurally valid. The responsible lawyer owns the legal theory, source authority, factual characterization, strategic judgment, and final filing decision.

Candidate checked statements

Possible controlled-English candidates are:

  • “For every asserted claim, if a required element lacks a linked evidentiary basis, the claim requires attorney review.”
  • “If service is confirmed and the response deadline is approved, the response task has a scheduling obligation.”
  • “Every dispositive-motion recommendation requires an approved issue statement and a supporting record reference.”

Example architecture

The matter platform supplies permissions and task state; docketing supplies lawyer-approved dates; document review supplies evidence identifiers. A versioned issue graph holds counsel-authored elements. FF Scribe checks a proposed statement and produces deterministic readbacks linked to—not substituted for—the graph and deadline system. Filing, waiver, preservation release, and client communication require human approval. Session logs are governed as potentially privileged work product.

Where verified readback fits

The attorney describes the desired issue or readiness rule in ordinary professional language. A model produces a single setup-constrained proposition or asks for clarification. Agda accepts or rejects its formal construction; bounded repair can address compiler diagnostics. A well-typed structure within the configured readback slice yields the finite deterministic family, while unsupported translation fails visibly. The attorney compares a successful reading with the intended theory and provides explicit acceptance or feedback. Passing the type checker is not proof completion, and acceptance is not an adjudication of law or fact; it records only that counsel recognizes the checked statement as the intended internal proposition.

Potential benefits

The assistant can expose hidden assumptions, improve issue-outline consistency, and link an internal rule to counsel-approved wording. It may reduce missed dependencies, support case reviews, and distinguish absent evidence from a negative finding. Litigators need not read Agda.

Limits/adoption considerations

Adversarial facts, evolving theories, local practice, and tactics resist rigid encoding. Vocabularies must be narrow and matter governed; disputed propositions need explicit status. Deadline systems require independent validation and attorney review. Organizations need privilege labeling, supervisory controls, conflict screening, audit access, and setup-supersession procedures.
04Legal change-impact and interpretation comparison service

System/use case

A legal change-impact service lets counsel compare proposed interpretations or rule versions before changing established guidance, controls, forms, or decision procedures. It represents dependencies among defined terms, scope conditions, exceptions, obligations, and recommendations so affected propositions can be reviewed deliberately.

Operational setting

The service supports horizon scanning and policy governance using source snapshots, counsel-authored change notes, accepted propositions, affected processes, and representative scenarios. It can compare counsel-curated setups but does not decide which text or interpretation controls.

Decision/claim boundary

The formal claim is limited to the structural consequences expressed by a selected version—for example, that a newly defined covered category entails an additional assessment step. A successful check does not prove the amendment’s legal effect, forecast enforcement, validate a scenario’s facts, or show that all downstream impacts were found. Counsel approves the authoritative source, effective period, interpretive assumptions, and operational disposition.

Candidate checked statements

Illustrative comparison candidates include:

  • “Under the proposed rule version, every newly covered service has a documentation obligation.”
  • “If the revised definition applies to an existing matter, that matter requires applicability reassessment.”
  • “If two approved rules assign incompatible dispositions to the same classified case, the case requires legal escalation.”

Example architecture

A source store and dependency graph map rules to accepted propositions, controls, templates, and requirements. Counsel curates baseline and proposed setups. A runner submits representative statements to FF Scribe and records compiler outcomes and readback IDs. A diff service compares structures and downstream references; a dashboard assigns impacts. Approved interpretations pass through existing change gates, with old setups retained for reproducibility.

Where verified readback fits

An authorized lawyer states an expected consequence for a selected baseline or proposed setup. The model translates it into that setup’s finite vocabulary, and Agda checks the proposition’s type. If its structure is supported, the audited readback family deterministically exposes quantified entities, premises, and conclusion; otherwise translation stops visibly. The lawyer accepts a successful reading or supplies feedback, producing a versioned, reviewable proposition for comparison. Type correctness is distinct from legal truth; a checked statement may be incomplete, based on an unauthorized interpretation, or inconsistent with user intent until professional review is complete. Nor does the workflow construct a proof that the conclusion follows from real-world facts.

Potential benefits

The service can reveal decisions relying on changed definitions, compare interpretations in stable language, and prioritize widely connected controls. It preserves why guidance changed and surfaces conflicts before implementation. Reviewers see formal structure and lawyer-approved readback, not opaque generated recommendations.

Limits/adoption considerations

Completeness depends on the dependency inventory and the quality of counsel’s setups. Temporal rules, transitional provisions, cross-jurisdiction interactions, and non-textual authorities may require specialized modeling or remain unsupported. The service needs rigorous source provenance, semantic versioning, dual review for high-impact changes, deprecation rules, and monitoring for stale accepted statements. Operational impact analysis and authoritative legal judgment remain human-led activities.
MLTTDB4 patterns
This catalogue develops the definitions, jurisdiction, obligation, deadline, and consistency themes in ~/nn-ff-web/content/domains/legal.md. The designs are illustrative, jurisdiction-neutral architecture sketches rather than legal advice. Every formalization, rule release, and case-specific use requires review by appropriately qualified legal professionals.
01Contract obligation lifecycle assurance

Operational context

A commercial legal-operations team maintains a portfolio of negotiated supply, outsourcing, and services agreements. Obligations arise from events such as an effective date, acceptance, renewal notice, service failure, or termination. The contract repository holds executed documents, while matter owners need a dependable view of which normalized obligation templates, trigger categories, notice routes, and evidence requirements can coexist. The hard problem is not merely extracting clauses: it is preventing a reviewed obligation catalogue from acquiring impossible dates, incompatible trigger/actor combinations, or dangling references as lawyers refine it.

Why MLTTDB fits

Counsel can define the admissible vocabulary and invariants as proof-assistant types: a notice obligation must name an obligated party, recipient role, trigger, period convention, and permitted delivery channel; a cure right can only refer to an earlier breach-notice pattern. Analysts can then edit ordered, UUID-addressed source terms without weakening those types. Agda finite lookup is useful when a reviewed obligation row refers to a previously declared trigger or notice pattern. If the organization standardizes on Lean or Rocq, the model should instead use generated identifiers or self-contained rows because their current preprocessors do not implement finite table lookup.

Example architecture

executed contracts -> extraction/reconciliation -> lawyer review workbench
                                                  |
proof model repo -> CI ----> MLTTDB SQLite <-------+ curated typed records
                       fetch/orchestrate verify -> Agda/Lean/Rocq -> evidence bundle

The repository owns types, declarations, contract-family modules, and propositions. An external extraction service proposes clause spans and source coordinates; the workbench requires a lawyer to accept or correct them and writes only normalized, source-language records to MLTTDB. Verification runs against a pinned model revision. A separate obligation-management platform consumes only approved exports and executes reminders, assignments, and escalations.

Representative typed artifacts

The model could declare triggerPatterns :T: TriggerPattern, noticePatterns :T: NoticePattern, and obligationTemplates :T: ObligationTemplate. Types distinguish calendar from business-day periods, one-off from recurring duties, and conditions precedent from post-trigger duties. A proposition such as wellFormedObligation checks that the selected action is available to the actor role, required evidence matches the action, and any referenced notice or cure pattern is compatible. External metadata links each UUID to agreement, clause span, reviewer, and approval record; those links are not proof of the contract text’s truth.

Checks and evidence

CI exercises schema mode before analysts receive a new model. Data-mode verification then checks every current record and emits proof-assistant diagnostics and generated source where applicable. A release job records the model commit, database snapshot identifier, ordered UUID list, verification output, tool versions, and legal approvals in an external evidence repository. Negative fixtures cover unknown references, invalid party roles, contradictory duration conventions, and cycles. Sampling compares normalized terms back to executed clauses.

Potential benefits

The team gains earlier detection of catalogue inconsistencies, a reviewable separation between legal semantics and portfolio data, and repeatable regression checks when templates change. UUIDs support stable discussion of rows, while ordering makes review exports deterministic. The evidence bundle can show exactly what was checked and under which model without claiming that the software interpreted the agreement conclusively.

Deployment boundary

MLTTDB does not extract clauses, determine contractual meaning, establish that an event occurred, send notices, calculate authoritative deadlines, or enforce an obligation. The contract repository and approval system remain systems of record. Runtime reminders must fail safely and expose their source assumptions. Privilege, confidentiality, retention, legal hold, access segregation, and professional review require controls outside MLTTDB; a qualified lawyer approves every template and matter-specific conclusion.
02Litigation and regulatory deadline rule regression

Operational context

A docketing function supports disputes and regulated submissions across multiple forums. Deadline rules combine event type, service method, counting convention, excluded days, extensions, and discretionary orders. The organization already has a docketing engine and authoritative calendars, but changes to its rule packs are difficult to review: a revised definition may alter thousands of scenarios, and a malformed rule can silently omit a required input. The proposed system is a pre-release assurance environment for rule packs, not the live calendar.

Why MLTTDB fits

Formal row types can make each rule explicit about forum profile, triggering event, period, counting method, adjustment policy, and authority reference. Scenario tables can encode reviewed inputs and expected structural outcomes. An external rule-pack compiler can materialize a reconciled DeadlineRuleManifest aggregate term. Proofs can then establish properties such as “a computed due date is not earlier than its trigger” under the modeled calendar assumptions, or that every mandatory event class enumerated by the manifest maps to exactly one applicable rule in a selected profile. Ordered records make regression suites stable, and UUIDs give reviewers durable handles across revisions.

Example architecture

authority monitoring -> counsel-authored rule proposal -> rule-model branch
authoritative calendars -> scenario builder -> MLTTDB scenario/rule records
model and records -> proof-assistant validation -> evidence review -> release gate

Legal researchers monitor authorities in an external service. Counsel translates approved changes into a model branch and curated records. A calendar adapter snapshots the holidays and closure assumptions used for testing. Each regression scenario carries a counsel-reviewed declared DeadlineResult and witness under the selected rule-pack model. MLTTDB supplies those rows to the proof-assistant validation path. A release-gate service compares the checked declarations with the previous approved pack and routes material differences to docketing counsel before a separate deployment mechanism updates the operational engine; generic data-mode output is not treated as a computed calendar-result API.

Representative typed artifacts

Tables might include forumProfiles :T: ForumProfile, deadlineRules :T: DeadlineRule, and regressionScenarios :T: DeadlineScenario. DeadlineRule can require an effective interval, event kind, duration, day-count basis, service adjustment, and precedence class. DeadlineScenario includes the reviewed inputs, a declared DeadlineResult, and a witness that the selected model relates those inputs to that result. The model can represent an explicit AuthorityRef as a typed identifier with review status, while leaving the authoritative text in the legal research system. In Agda, a scenario could refer by UUID to an earlier rule or forum row; Lean/Rocq deployments should materialize an equivalent generated definition structure without assuming that lookup feature.

Checks and evidence

Schema checks reject declarations that no longer elaborate. Data checks reject missing fields, malformed rule alternatives, illegal references, and declared-result witnesses that fail. The regression harness compares checked declarations for boundary scenarios around excluded days, service adjustments, effective-date transitions, and overriding orders. Review output should include old/new declared results, changed model and row UUIDs, calendar snapshot identity, proof-assistant diagnostics, comparator version, and explicit counsel disposition. Independent reconciliation against a sample from the production docketing engine detects translation drift.

Potential benefits

Rule-pack changes become inspectable before they reach live matters. Reviewers see which assumptions and scenarios changed rather than receiving an opaque code diff. Typed cases reduce structurally incomplete rules, and propositions catch contradictions that ordinary field validation misses. The organization can retain reproducible review evidence for internal quality assurance while keeping its existing docket workflow and escalation practices.

Deployment boundary

MLTTDB does not research authorities, decide which rule controls, know whether service was effective, maintain an authoritative court calendar, docket a matter, or guarantee a deadline. Court orders and professional judgment can override modeled defaults. The live system needs dual review, clock and calendar governance, urgent exception handling, access controls, monitoring, and tested fallback procedures. No deadline is released or relied upon without qualified counsel and docketing review.
03Data-processing and transfer clause pre-decision review

Operational context

Privacy counsel reviews data-processing agreements, security schedules, subprocessor terms, and cross-border transfer provisions during vendor onboarding. A questionnaire and contract-analysis service can identify candidate facts, but the review team must determine whether the proposed clause set contains required concepts for the intended processing profile and whether negotiated deviations are internally coherent. Terminology varies across templates and jurisdictions, so the architecture focuses on organization-approved control patterns rather than asserting a universal legal test.

Why MLTTDB fits

A proof-assistant model can distinguish roles, processing purposes, data categories, transfer situations, safeguard families, audit commitments, deletion duties, and exception approvals. MLTTDB lets analysts maintain proposed agreement profiles and clause-pattern selections as typed source terms while the semantic checker enforces relationships defined by privacy counsel. For example, the model can reject a profile that selects a transfer mechanism incompatible with its modeled party roles, or requires a supplementary-control assessment but supplies no reviewed assessment reference.

Example architecture

vendor intake and contract -> extraction/classification -> privacy review UI
approved clause library ----> formal-model mapping -----> MLTTDB records
model repo and records -> proof-assistant verification -> approval workflow

The intake platform owns vendor identity, processing facts, attachments, and source text. Extraction proposes mappings with confidence and text spans. A privacy professional confirms those facts and chooses approved clause patterns in the review UI. An adapter renders the reviewed selections as source-language records. Store-orchestrated or CI verification invokes Agda, Lean, or Rocq; a findings service translates checker output into reviewer-facing language and sends dispositions to the existing third-party risk workflow.

Representative typed artifacts

Possible declarations include processingProfiles :T: ProcessingProfile, clauseAssessments :T: ClauseAssessment, and deviationApprovals :T: DeviationApproval. Sum types prevent conflating controller/processor role claims with transfer-role claims. A ClauseAssessment carries a clause-family identifier, applicability rationale category, reviewer-confirmed source span reference, and disposition. A reconciled ClauseCoverageManifest aggregate term enumerates counsel-designated categories, accepted patterns, deviations, and assessment UUIDs; proof obligations can require every category represented there to be satisfied by an accepted pattern or an authorized deviation. Agda lookup can connect an assessment to earlier approved pattern rows; the other current backends need self-contained or generated references.

Checks and evidence

Validation checks the reconciled manifest’s coverage of counsel-designated requirement categories, typed compatibility of role and safeguard selections, effective intervals for approved patterns, and absence of reference cycles in the represented dependency graph. Scenario suites model representative vendor arrangements and negotiated combinations, including negative cases for missing subprocessors, incompatible deletion commitments, and lapsed deviations. Evidence should pair the checker result with the formal-model revision, ordered record snapshot, manifest reconciliation, confirmed clause spans, extraction-versus-review changes, and named legal approval. Source text remains independently retrievable from the contract system.

Potential benefits

The approach can reduce inconsistent application of an internal clause playbook, expose missing review inputs before signature, and make deviations easier to compare across vendors. Formal types turn ambiguous dropdown combinations into explicit modeling questions. Repeatable scenarios help privacy teams understand the operational effect of playbook revisions, and retained evidence distinguishes machine-proposed mappings from lawyer-confirmed conclusions.

Deployment boundary

MLTTDB does not classify parties conclusively, establish where processing occurs, determine legal adequacy, monitor legal change, draft negotiated text, or authorize a transfer. Extraction confidence is not evidence of a legal fact. Data mapping, vendor identity, document custody, access, privilege, retention, and workflow remain external. Counsel must approve the formal categories, jurisdiction-specific overlays, exceptions, and every agreement disposition before contracting or data movement proceeds.
04Insurance-claims coverage and denial-reason packet assurance

Operational context

An insurer’s coverage unit and legal function review complex property, casualty, or specialty claims before issuing a reservation-of-rights, partial coverage, or denial communication. The claim system contains loss notices, investigation material, adjuster findings, and payment activity; the policy administration system holds declarations, forms, endorsements, and effective periods. The assurance problem is whether a proposed coverage-position packet uses the reviewed policy-form set, distinguishes established findings from open questions, and connects each proposed reason to the applicable insuring agreement, condition, exclusion, or endorsement. It is not an automated coverage determination.

Why MLTTDB fits

Coverage counsel can define typed abstractions for policy-form profiles, coverage provisions, endorsements, exclusions, conditions, confirmed findings, unresolved issues, position categories, communication reasons, and complaint or appeal routes. A packet term can carry the adjuster’s reviewed findings and the proposed position together with witnesses that each reason is permitted by the selected internal model. Type distinctions can prevent an allegation or unverified investigation item from being used as a confirmed predicate. Separating the legal model from case packets also permits synthetic regression when an approved form interpretation or reason template changes.

Example architecture

policy administration + claims/evidence system
                  |
      adjuster-confirmed findings and form reconciliation
                  v
       MLTTDB typed coverage-position packet
                  |
       Agda/Lean/Rocq validation status and diagnostics
                  v
 coverage counsel review -> correspondence workflow -> claim file

Policy administration and claims platforms remain the systems of record. A projection service resolves the in-force form and endorsement identifiers, preserves source references, and reports reconciliation gaps. The term store holds a minimal, preferably pseudonymized packet under a pinned legal-model revision. The proof assistant validates its typed declarations; a project-owned adapter maps native diagnostics and UUIDs into the counsel workbench. Authorized reviewers record their interpretation and approve any communication through the existing claims workflow.

Representative typed artifacts

Declarations could include formProfiles :T: PolicyFormProfile, coveragePackets :T: CoveragePositionPacket, and communicationReasons :T: CoverageReason. A PolicyFormProfile identifies the reviewed declarations, base form, endorsements, and effective interval without storing the authoritative documents. CoveragePositionPacket separates reported assertions, investigator-confirmed findings, disputed facts, unresolved coverage questions, proposed disposition, and escalation state. A reason artifact relates one reviewed provision and finding category to a proposed explanation; it does not assert that the provision controls as a matter of law. Agda lookup may connect a packet to an earlier form-profile row, while a portable design uses self-contained or ordinarily generated associations.

Checks and evidence

Validation can reject an unknown or out-of-period form profile, a reason that is not permitted for the declared position category, a cited endorsement absent from the reviewed form set, an unresolved question represented as a confirmed finding, or a proposed communication without the modeled review or complaint route. Synthetic regression packets should cover conflicting endorsements, multiple causes of loss, late or incomplete information, reservation states, partial coverage, and reason-template changes. External evidence should bind the policy and claim revisions, projection reconciliation, formalization commit, ordered row UUIDs, checker diagnostics, counsel comments, approval record, and final correspondence hash.

Potential benefits

Coverage reviews can become more consistent about form selection, finding status, reason provenance, and escalation. Typed packets can expose structural gaps before correspondence is issued, while stable UUIDs make legal comments and remediation traceable. Regression cases show which reviewed packets no longer validate after a model or template change without presenting that result as a substantive coverage conclusion.

Deployment boundary

MLTTDB does not read a policy conclusively, decide which provision controls, assess credibility or causation, determine coverage or bad-faith exposure, value a loss, authorize payment, draft legal advice, issue correspondence, or resolve a complaint or appeal. Privilege, confidentiality, document custody, fair-claims handling, jurisdiction-specific duties, deadlines, access control, and human authority remain external. Qualified coverage professionals and counsel must approve the form mapping, formal model, case-specific interpretation, and every consequential communication.
State Machine Studio3 demos
SMPublic-Benefit Adjudication and Appeal

This example represents a public-benefit case from application through an appealable, reasoned determination. It is deliberately program-neutral: the controlling definitions, thresholds, exclusions, filing rules, and review rights can be supplied for a particular benefit and jurisdiction. The model’s concern is procedural integrity—using the right rule version, building a complete record, explaining the result, and preserving a genuine route for review.

The ordinary case begins by recording the benefit sought, filing jurisdiction, application date, and applicant identity. Evidence review maps the submitted record to required categories, requests missing or stale material, and tracks response deadlines and authorized extensions. Once the record is sufficiently complete, eligibility determination applies the definitions and criteria effective for the case, considers thresholds, exclusions, and stated exceptions, and records the rule path for each finding. A separate decision review checks the proposed outcome, reasons, and citations before accountable approval. The issued notice communicates the outcome, reasons, effective date, and applicable appeal window. If no appeal is filed in time, the operative outcome is closed and retained.

The return paths protect both the claimant and the deciding authority. Invalid intake can be corrected without silently losing the original filing context. Missing evidence sends the matter back to evidence development. Inconsistent reasoning is remanded before a decision is issued. A timely appeal reopens contested findings and permits supplemental evidence; the reviewer may affirm, revise, or remand. A remand can return to evidence collection, while an appeal outcome is reissued with a renewed operative decision. These controls matter because eligibility is not merely a yes-or-no calculation: jurisdiction, effective dates, notice, deadlines, review authority, and an auditable explanation can determine whether a legally correct result was reached through a fair process.

Layer 1 — Adjudication stages

This layer shows the case-level progression used by program counsel, supervisors, and appeals staff: intake, evidence development, eligibility determination, decision review, issuance, appeal, and closure. It exposes remands and reopening paths without overwhelming the reader with individual documents. It intentionally excludes caseworker keystrokes and criterion calculations so procedural posture and decisional authority remain clear.

Layer 2 — Eligibility and appeal procedures

This layer expands each stage into the procedures that establish a defensible administrative record. It includes evidence-category mapping, deadline management, application of effective definitions, reason drafting, citation checking, accountable review, timeliness analysis, and reconsideration of contested findings. It is appropriate for policy manuals and quality assurance. It does not encode the substantive formula for any one benefit program.

Layer 3 — Caseworker actions

This layer identifies the concrete work items performed on a case: recording filing facts, issuing a request for evidence, documenting an extension, evaluating each criterion, checking rule versions, calculating the appeal window, and preserving notices and review history. It supports task assignment and audit reconstruction. Jurisdiction-specific forms, document templates, and system screen interactions are intentionally left to the implementing agency.
Open interactive model
SMMulti-Jurisdiction Contract Obligations

This example models obligation management for a contract whose duties are distributed across the main agreement, schedules, amendments, and jurisdiction-specific overlays. It treats a contract as an active network of defined terms, triggering events, responsible parties, notice mechanics, deadlines, exceptions, and remedies—not as a static signed PDF.

The workflow starts by identifying the operative document set, incorporated materials, governing law, parties, and effective dates. Clause mapping normalizes defined terms, resolves document precedence, extracts conditions and exceptions, and assigns each obligation to a responsible party. Once activated, monitoring watches for events such as delivery milestones, renewals, consent requests, volume thresholds, or termination dates, then recalculates the relevant windows. A triggered obligation becomes due: the responsible party is notified, evidence of payment, delivery, consent, or notice is collected, and performance is tested for timeliness and contractual sufficiency. Satisfied performance returns the contract to active monitoring. At term, surviving duties and final notices are resolved before closure.

The machine also preserves the legal response when performance is incomplete or disputed. An incorrect document set returns to intake because downstream conclusions cannot safely rest on missing amendments. An unmet obligation moves into breach and cure, where the duty, available remedy, required notice, cure period, corrective action, and reservation of rights are tracked. A completed cure can restore monitoring; a disputed cure reopens the obligation for evaluation; an uncured material breach may close the relationship through the authorized termination path. These controls matter to contract managers and counsel because missed dependencies often arise from cross-references and changing dates, while an otherwise valid remedy can be lost through defective notice or failure to preserve rights.

Layer 1 — Contract lifecycle

This layer provides the portfolio and matter-level view: intake, clause mapping, active monitoring, performance due, breach and cure, and closure. It shows when the contract is merely being interpreted versus when a live duty or remedy is in play. It intentionally excludes clause-by-clause extraction details so counsel and contract owners can see the operative posture quickly.

Layer 2 — Obligation management procedures

This layer describes how the legal operations team turns text into controlled work. It includes normalizing definitions, applying precedence, associating duties with parties, monitoring triggers, calculating notice and renewal windows, evaluating evidence, issuing cure notices, and tracking reservations of rights. It is suitable for playbooks and workflow configuration. It excludes the wording of any particular negotiated clause.

Layer 3 — Clause-level actions

This layer exposes the individual actions used to support a conclusion: identify an incorporated schedule, map a defined term, record an exception, apply a jurisdictional overlay, notify an owner, collect proof of performance, and archive the evidence timeline. It enables review of exactly how an obligation was derived and handled. Document-specific citation coordinates, email templates, and repository APIs are intentionally implementation details beyond this example.
Open interactive model
SMRegulatory Matter and Deadline Management

This example represents the controlled response to a regulator, supervisory authority, or other rule-bound legal request. It covers preservation and collection, privilege and responsiveness review, preparation of an approved response, filing, follow-up, remediation, and closure. The model is intentionally neutral about the authority so its procedures can be adapted to an information request, examination, notice, subpoena, or similar matter.

Opening the matter establishes the issuing authority, jurisdiction, request scope, and the deadlines for response, preservation, and internal escalation. Scoped holds and collection instructions then identify custodians and sources, track completeness, and escalate unavailable or altered records. Privilege review classifies responsive material, records the applicable privilege grounds, applies redactions or withholding, and produces the supporting privilege record. Response preparation maps each requested item to produced material or a reasoned explanation, addresses missing items and exceptions, and obtains responsible legal approval. Filing uses the required channel, confirms receipt, and tracks follow-up, correction, extension, and remediation dates until all obligations are fulfilled.

Several loops prevent a superficially complete response from becoming an unreliable filing. Privilege review can return an incomplete collection for additional records. Response preparation can reopen collection when an evidentiary gap appears. A missed deadline, rejected submission, or scope dispute enters a matter exception rather than being handled informally. The corrective path may seek an extension, repair and resubmit the filing, reopen substantive preparation, or escalate for accountable approval. Closure occurs only after final obligations and holds have been resolved and the record of decisions, productions, filings, and evidence is preserved. These controls matter because defensibility depends on chain of custody, consistent privilege treatment, timely action, approval, and proof of receipt as much as on the prose of the response.

Layer 1 — Matter lifecycle

This layer gives lead counsel and matter managers the procedural posture: opened, collecting, under privilege review, preparing a response, filed and monitored, in exception, or closed. It highlights rework and corrective paths alongside the normal progression. It intentionally suppresses document-level decisions so leadership can assess scope, deadline risk, and accountability at a glance.

Layer 2 — Response and filing procedures

This layer covers the repeatable legal operations procedures within each posture: calculating deadlines, issuing preservation instructions, reconciling custodians and sources, applying review protocols, preparing a privilege record, mapping requests to responses, obtaining approval, confirming receipt, and managing remediation. It supports matter plans and quality gates. It excludes the substantive legal position taken in a particular response.

Layer 3 — Document-level actions

This layer exposes the concrete handling steps for records and filing components: classify responsiveness, identify a privilege basis, redact or withhold, explain a missing item, route a draft for approval, submit through the prescribed channel, and record confirmation. It supports production audits and exception investigation. Review-platform commands, file formats, and authority-specific portal mechanics remain outside the generic model.
Open interactive model
Explore patternsReview product applications

Cabinet index

Explore Formal Foundry

Search the archive

Find a page

Type to search the published content.