×

Finance

Challenges

  • Risk limits combine positions, entities, products, and changing market conditions.
  • Settlement workflows depend on timing, eligibility, and exception handling.
  • Controls must remain consistent across data sources and reporting boundaries.
  • Reviewers need reproducible explanations for alerts and calculated outcomes.

Problems We Solve

  • Constraint Modeling Represent limits, dependencies, and aggregation boundaries.
  • Limit Checking Evaluate positions and events against approved constraints.
  • Exposure Simulation Explore representative scenarios and threshold changes.
  • Settlement Validation Check prerequisites, timing rules, and exception paths.
  • Reporting Evidence Preserve traceable inputs and calculation decisions.

Domain portfolio

Application patterns

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

The Finance domain covers risk limits, settlement, and reporting across positions, legal entities, products, market conditions, timing, evidence, and system boundaries. These examples use FF Scribe to confirm precisely scoped financial propositions, not as a pricing engine, books-and-records platform, execution control, or source of financial truth. Each deployment needs an audited setup vocabulary and named authorities for limits, data, and decisions.
01 Pre-trade risk-limit authorization Explore pattern

System/use case

A control workbench formalizes the decision rules used when an order is checked against counterparty, issuer, product, concentration, and desk mandates before release. It is most useful for explaining composite alerts and documenting what an approver means when requesting a new limit rule or an exception path.

Operational setting

Order and execution systems submit the account, legal entity, product taxonomy, direction, notional, and exposure snapshot. A risk service calculates approved metrics and identifies the applicable limits. Breaches, stale inputs, and classification conflicts enter a supervised risk queue; the trading desk may contribute, but approval remains independent.

Decision/claim boundary

The checked claim should express the logical boundary of authorization—for example, which reviewed facts imply escalation or release. It must not claim that an exposure number is accurate, that a market scenario is valid, or that a limit is commercially or regulatorily appropriate. The accountable risk function approves the setup vocabulary and the proposition; operations technology owns correct system enforcement.

Candidate checked statements

The following are illustrative controlled-English propositions for a future setup, not statements already implemented by FF Scribe:

  • For every order and applicable limit, if the projected exposure exceeds the approved limit, then the order requires independent risk approval.
  • For every order, if the position snapshot is stale, then automated release is inhibited.
  • For every approved exception, if its validity period has ended, then it does not authorize order release.

Example architecture

Order and reference-data events flow through a normalization layer to the existing exposure and limit engines. Those engines return metrics, limit identifiers, timestamps, and reason codes to a decision-orchestration service. FF Scribe sits beside the governed rule-authoring and review workflow: it receives a practitioner’s proposed meaning plus a versioned setup, not an unrestricted trading feed. The accepted type, readback candidate ID, setup version, compiler outcome, and user confirmation are stored in an immutable rule-review record. Enforcement remains in the independently tested pre-trade control service. A risk officer is the meaning and approval authority; neither the model nor the compiler can release an order.

Where verified readback fits

A risk specialist describes the intended authorization condition in natural language. The model proposes one setup-scoped proposition using only registered entities and relations. Agda checks that the expression is syntactically and type correct. If the separate partial readback stage supports its structure, it produces the finite audited family without model-authored paraphrase; unsupported structure fails visibly. The specialist accepts a successful reading or supplies feedback. That acceptance confirms intended meaning only; it is not a proof that a limit was breached or that the production control enforces the rule.

Potential benefits

  • Reduces ambiguity when desk, risk, and engineering teams translate a policy decision into a control specification.
  • Preserves a reproducible statement, vocabulary version, and reviewer confirmation for model-risk, internal-control, and change-governance evidence.
  • Makes hidden premises such as snapshot freshness, entity attribution, and exception validity visible before implementation.
  • Supports consistent review of alert reasons without allowing an LLM to invent the final confirmation wording.

Limits/adoption considerations

Type correctness establishes that a proposition is well formed in the chosen setup; it does not establish factual exposure, limit calibration, model validity, policy compliance, or control effectiveness. FF Scribe checks proposition types, not proof objects, so a checked implication is not proof that its premises or conclusion hold for a live order. Practitioner acceptance confirms the readback matches intended semantics, not that intent is authorized. Market-data lineage, metric reconciliation, independent model validation, access segregation, latency testing, and production surveillance remain separate controls.
02 Securities settlement exception and release management Explore pattern

System/use case

A settlement-control application formalizes prerequisites and exception routes for delivery-versus-payment or receive-versus-payment instructions. It helps operations teams distinguish an unmatched instruction, an ineligible asset, missing inventory or cash, an invalid standing settlement instruction, and an approved hold or release.

Operational setting

Trade capture sends allocations and instructions to matching and settlement platforms. Custodian responses, inventory, cash projections, eligibility, calendars, and acknowledgements arrive asynchronously. Exceptions route to settlements operations, treasury, client service, or a control manager by reason and materiality. Existing venue and custodian adapters govern cut-off-sensitive actions.

Decision/claim boundary

The formalized proposition defines when a workflow may label an instruction ready, held, or escalated. It does not attest that securities or cash are available, that a custodian message is authentic, or that settlement finality has occurred. The settlement control owner approves rule meaning; operations staff remain accountable for exception disposition and any manual release.

Candidate checked statements

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

  • For every settlement instruction, if matching is confirmed and asset eligibility is confirmed, then the instruction is eligible for readiness review.
  • For every instruction, if the approved standing settlement instruction is absent, then automated release is inhibited.
  • For every settlement exception, if cash coverage is unresolved at the review cut-off, then the exception is escalated to the designated owner.

Example architecture

A canonical trade store correlates executions, allocations, and instruction versions. Event adapters ingest matching, custodian, depository, inventory, cash, and calendar status into a timestamped evidence ledger. A rules service computes operational status, while a case-management layer presents evidence and captures maker-checker actions. FF Scribe supports controlled rule review at configuration and change time. Accepted propositions and readbacks are linked to rule versions and test scenarios. The deterministic engine never sends settlement messages; authenticated adapters and dual-control workflows retain that capability. Human operators can reject stale or contradictory evidence and must record the basis of material overrides.

Where verified readback fits

An operations control designer states a proposed prerequisite or escalation rule in natural language. A model maps it to the finite vocabulary of the settlement setup. Agda type-checks the candidate. The partial readback translator then either renders supported structure through the deterministic audited family or reports unsupported structure without a partial reading. The designer explicitly accepts a successful reading or provides corrective feedback. This loop validates the shape and understood meaning of the proposition; it does not validate source messages, prove readiness, or authorize settlement.

Potential benefits

  • Produces reviewable rule specifications across operations, custody, treasury, and engineering terminology.
  • Makes exception classes and evidence prerequisites explicit, reducing conflation of “missing,” “failed,” “on hold,” and “not applicable.”
  • Links workflow changes to stable checked statements and human confirmations for regression design.
  • Improves post-incident reconstruction by preserving what reviewers believed a rule meant at a particular setup version.

Limits/adoption considerations

Temporal cut-offs, calendars, partial settlement, netting, finality, and venue-specific semantics need explicit modeling and cannot be inferred from ordinary language. A type-correct rule may still use stale or false facts, implement a poor operational policy, or disagree with a platform’s actual behavior. A checked proposition is not a completed proof of settlement eligibility. User confirmation is not maker-checker authorization. Reconciliation, message authentication, access control, resilience, and accountable manual decision-making remain mandatory.
03 Financial and management reporting reconciliation Explore pattern

System/use case

A reporting-evidence service formalizes assertions around source-to-report reconciliation, adjustment approval, aggregation boundaries, and sign-off readiness. Typical users are financial controllers, product control, regulatory reporting operations, data owners, and internal audit.

Operational setting

Subledgers, the general ledger, valuation stores, counterparty masters, and governed data platforms feed a reporting mart. Reconciliation jobs compare balances and record breaks by source, account, entity, product, currency, and reporting period. Manual adjustments and mapping overrides pass through controlled journals and reviewer queues before report production.

Decision/claim boundary

The checked proposition should identify the evidence conditions for a reconciliation or sign-off state. It does not certify accounting treatment, valuation, completeness of source populations, control effectiveness, or the truth of a published report. The report owner and financial control authority decide whether evidence is sufficient and approve any attestation.

Candidate checked statements

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

  • For every report line and source balance, if the report line is mapped to the source balance and the reconciled variance is within the approved tolerance, then the line is eligible for controller review.
  • For every material break, if remediation evidence is absent, then period sign-off remains pending.
  • For every manual adjustment, if independent approval is recorded, then the adjustment is eligible for inclusion review.

Example architecture

Versioned connectors load extracts into a lineage catalog and reconciliation engine. Results, variances, mappings, tolerances, and data-quality flags enter an evidence store. A workflow assembles period sign-off packs with adjustment approvals and unresolved breaks. FF Scribe supports rule and attestation-template governance; each accepted proposition links to lineage, calculation version, control owner, and tests. Controllers decide sufficiency, and the tool cannot post journals or issue reports.

Where verified readback fits

A controller describes a readiness or escalation assertion. The model proposes a proposition limited to the reporting setup’s registered vocabulary. Agda checks the candidate type. For supported structure, audited deterministic readback produces the controlled finite family while preserving premise order and provenance; unsupported translation fails visibly. The controller accepts a successful reading or corrects it through feedback. The outcome is an intent-confirmed specification—not evidence that mappings are complete, balances agree, or a report is fairly presented.

Potential benefits

  • Creates a common, reproducible description of reconciliation and sign-off criteria across finance and data teams.
  • Exposes aggregation scope, tolerance, materiality, approval, and period dependencies that are often buried in prose or spreadsheets.
  • Provides stable inputs for test cases, control walkthroughs, and change-impact reviews.
  • Separates the model-generated candidate from compiler authority, deterministic readback, and controller acceptance.

Limits/adoption considerations

Accounting judgment, materiality, reporting perimeter, valuation methodology, and source completeness require accountable professional review. Type checking cannot establish factual truth or reporting compliance, and it does not test whether the implemented reconciliation behaves like the proposition. Proposition checking also does not complete a proof that sign-off conditions hold. Confirmation records user intent at that moment; it does not substitute for an authorized sign-off, control-performance evidence, or audit conclusion.
04 Liquidity and collateral eligibility governance Explore pattern

System/use case

A treasury decision-support platform formalizes eligibility, concentration, haircut, substitution, and escalation statements used in collateral allocation and liquidity-buffer review. The aim is to make rule meaning reviewable before it is encoded in optimization and operational systems.

Operational setting

Inventory services supply security identifiers, ownership, encumbrance, location, and availability. Eligibility masters, agreements, limits, valuations, haircuts, and projected obligations feed an allocation engine. Treasury and collateral operations review shortfalls, substitutions, and disputed classifications; independent treasury risk owns limits and challenge.

Decision/claim boundary

A checked proposition can express conditions under which an asset is eligible for allocation review or a shortfall requires escalation. It does not prove title, asset availability, valuation accuracy, legal enforceability, optimal allocation, or adequate liquidity. Treasury risk and the designated collateral authority remain accountable for classifications, limits, and overrides.

Candidate checked statements

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

  • For every asset and obligation, if the asset satisfies the approved eligibility class and remains unencumbered, then it is eligible for allocation review.
  • For every collateral pool, if the projected concentration exceeds the approved threshold, then the pool requires treasury-risk review.
  • For every proposed substitution, if equivalent coverage is not established, then release of the original collateral is inhibited.

Example architecture

A governed reference-data layer normalizes asset, counterparty, agreement, and eligibility identifiers. Valuation, haircut, inventory, concentration, and optimization services publish versioned results with timestamps and data lineage. An orchestration layer creates review cases and retains pre- and post-decision snapshots. FF Scribe supports the policy-to-rule review path, and its accepted proposition, deterministic readback, setup hash, and practitioner response become part of the rule’s approval package. Allocation execution remains behind existing entitlements, dual control, and downstream confirmation; humans adjudicate conflicting agreements or data.

Where verified readback fits

A treasury specialist states the intended eligibility or escalation rule in natural language. A model proposes a setup-scoped Agda type, and Agda checks type correctness. If the partial readback implementation supports that structure, it returns the deterministic finite family; otherwise the workflow fails visibly. The specialist explicitly accepts a successful reading or gives feedback for revision. No step demonstrates that the asset satisfies the premises, proves adequacy, or confirms that the optimizer used the rule.

Potential benefits

  • Aligns treasury, legal, risk, operations, and engineering on precise eligibility and exception semantics.
  • Preserves traceable rule intent across agreement, reference-data, and optimization changes.
  • Makes human override and escalation boundaries explicit before automation.
  • Supplies stable propositions for scenario design and implementation conformance testing.

Limits/adoption considerations

Agreement interpretation, legal enforceability, liquidity stress assumptions, haircut suitability, and optimization quality are outside type checking. Real-time availability and valuation remain factual inputs requiring independent controls. A well-typed proposition is neither a proof that coverage exists nor evidence that the production process is effective. Practitioner confirmation establishes understood intent only; formal rule approval and allocation authority must remain segregated, authenticated, and auditable.

Applicability frame

MLTTDB can validate finite catalogs of reviewed financial rules and cases. Proof-assistant source owns row types, :T: declarations, and semantic predicates. The SQLite term store owns ordered source-language terms, UUIDs, projection values, language metadata, and stored table definitions; Agda, Lean, or Rocq does the semantic checking. The store may orchestrate verification but does not calculate authoritative exposure or decide an outcome. Agda currently permits literal-UUID lookup of known same-table rows (which are dependency-ordered for generated checking) and rows from earlier-declared tables; Lean and Rocq preprocessors do not provide that finite lookup. Market/trade ingestion, golden-source reconciliation, clocks, pricing, identity and access, workflow, runtime controls, books and records, and regulatory interpretation remain external.

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, graph acyclicity, or aggregate lineage, 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 assurance.

01 Pre-trade limit rule release assurance Explore pattern

Operational context

An institutional trading platform maintains pre-trade rules for counterparty, issuer, product, desk, concentration, tenor, and mandate limits. Production engines combine positions, orders, reference data, prices, netting sets, and intraday utilization under strict latency constraints. Before a rule package is promoted, market-risk and technology teams need evidence that aggregation scopes are well-formed, limit precedence is unambiguous, exception routes are explicit, and representative boundary scenarios produce results consistent with the approved policy model.

Why MLTTDB fits

The release artifact is a finite catalog of limit definitions, scope relations, and scenario witnesses. Proof-assistant types can distinguish currencies, products, legal entities, and aggregation levels while encoding invariants such as scope containment and threshold ordering. MLTTDB can hold reviewed rule instances and boundary cases separately from the formal model, then rerun them as definitions change. It is appropriate for offline assurance, not low-latency order admission.

Example architecture

limit inventory + mandate system + risk taxonomy
                     |
     external rule compiler and reconciler
                     v
       MLTTDB candidate release catalog
                     |
        project-owned CI validation
                     v
          proof-assistant checker
                     |
 checked scenarios + executable-engine test vectors
                     v
   risk approval and production rule deployment

The compiler maps authoritative limit records into reviewed proof-language terms, retains source identifiers, and reports omissions or ambiguous taxonomies. A formal-policy repository defines scopes, precedence, and scenario semantics. The term store preserves catalog order and UUIDs. CI runs the proof checker plus parity tests against the actual pre-trade engine. A separate deployment service enforces entitlements, approvals, effective times, and rollback.

Representative typed artifacts

Candidate types include LegalEntity, TradingBook, RiskFactor, AggregationScope, Limit scope measure, Utilization measure, and BoundaryCase. Tables could be approvedScopes :T: AggregationScope, limitRules :T: LimitRule, and releaseCases :T: BoundaryCase. A compiler-reconciled LimitReleaseManifest aggregate term enumerates the scopes, precedence relations, limit rules, exceptions, and boundary-case UUIDs used for release-wide checks. A concentration limit term can carry proof that its child scopes are contained in the parent mandate and that warning thresholds do not exceed the hard limit. Scenario terms use supplied, normalized quantities rather than querying live positions or prices.

Checks and evidence

The checker can reject inconsistent units, orphan scopes, duplicate precedence for the same modeled condition, a soft threshold above a hard threshold, or an exception class not permitted for a mandate. It can prove expected classifications for zero, just-below, at-limit, and just-above boundary cases under the abstract semantics. Evidence should bind the typed snapshot to source inventory versions, transformation report, proof revision, checker output, production-engine build, and parity-test results. MLTTDB does not establish current utilization, valuation accuracy, booking completeness, market-data quality, or runtime engine behavior.

Potential benefits

Risk and engineering teams get an explicit, reviewable rule semantics rather than relying exclusively on configuration diffing. Type distinctions reduce category and unit errors, while reusable boundary proofs improve regression coverage when aggregation taxonomies or precedence change. Stable row identifiers help link limits, approvals, incidents, and model changes.

Deployment boundary

Run MLTTDB in the rule-authoring and release pipeline, isolated from the synchronous order path. A passing result is one input to approval, never an authorization to trade or deploy. Production kill switches, independent controls, entitlements, observability, reconciliation, and rollback remain mandatory. Qualified risk owners and formal reviewers must validate the abstraction, and engine parity must be demonstrated separately.
02 Settlement instruction and lifecycle rule validation Explore pattern

Operational context

A securities operations function maintains standing settlement instructions and lifecycle rules across legal entities, accounts, custodians, markets, instruments, settlement methods, and currencies. Misaligned account ownership, invalid market/currency combinations, or unclear instruction precedence can cause repair queues and settlement failure. Operations teams need a controlled way to validate proposed reference-data changes and modeled instruction selection before activation.

Why MLTTDB fits

Instruction eligibility and precedence can be represented as a finite typed relation: an instruction is valid only for a declared party, account, market, asset class, method, and effective-status input. MLTTDB can store reviewed reference terms and test cases and use a proof assistant to establish uniqueness or explicit ambiguity handling under the modeled selection rules. Explicit priority and specificity fields in an aggregate instruction manifest carry preference semantics; the store’s stable order supplies deterministic presentation and generated-definition emission only.

Example architecture

SSI master + security master + account/custodian records
                        |
      external reconciliation and candidate adapter
                        v
    operations four-eyes review in staging workspace
                        |
          MLTTDB instruction catalog
                        |
      store-orchestrated proof verification
                        v
     consistency report + downstream test fixture
                        |
   reference-data activation and settlement platform

Authoritative masters remain outside MLTTDB. The adapter resolves identifiers, proposes terms, and produces unmatched-record and effective-date reports. Operations reviewers confirm candidates. The term store can launch the configured backend, but the checker supplies semantic success or diagnostics. Activation, maker-checker approvals, message generation, sanctions controls, and settlement processing remain with existing platforms.

Representative typed artifacts

Types might include Party, SafekeepingAccount party, CashAccount party currency, Market, InstrumentClass, SettlementMethod, InstructionScope, and StandingInstruction scope. Tables such as accounts :T: AccountBinding, instructions :T: SettlementInstruction, and selectionCases :T: SelectionCase can express ownership and admissible combinations. An InstructionSelectionManifest aggregate term, built by the reference-data adapter and reconciled to the master-data and row exports, materializes scopes, explicit priorities, accounts, instructions, and representative cases for whole-snapshot checks. In Agda, an instruction row can refer to an earlier approved account by UUID finite lookup. In Lean or Rocq, relationships must use ordinary generated definitions or be embedded in supported row structures.

Checks and evidence

Validation can ensure that modeled cash and safekeeping accounts belong to the declared entity, selected currencies and markets are permitted, preference ranks are unique within an overlapping scope, fallback is explicit, and every supplied representative case resolves to exactly one instruction or a deliberately modeled exception. The release packet should include master-data snapshot IDs, adapter reconciliation, reviewed MLTTDB export, proof model and checker versions, diagnostics, downstream message-schema tests, and approval record. The proof does not authenticate instructions, determine real-time eligibility, screen parties, predict settlement, or verify an external custodian’s acceptance.

Potential benefits

Typed staging can catch referential and scope errors before instructions enter high-volume processing. Explicit selection proofs clarify why a representative trade selects a particular instruction and make precedence changes easier to regression-test. Persistent UUIDs provide durable linkage between catalog entries, repair incidents, and review decisions.

Deployment boundary

Use this as pre-activation reference-data assurance, never as the live settlement instruction resolver unless a separately engineered and validated runtime implements the approved semantics. Restrict catalog administration through external IAM and dual control. Operations, treasury, legal, compliance, and custodian-management specialists must review applicable fields, and independent reconciliations must confirm that activated downstream records match the approved snapshot.
03 Collateral eligibility and haircut configuration Explore pattern

Operational context

A collateral management function configures eligibility schedules and haircuts by agreement, counterparty, issuer, asset class, rating band, currency, maturity bucket, concentration tier, and liquidity characteristics. The operational engine consumes positions and valuations, while policy teams approve rule matrices and overlays. Configuration changes risk creating uncovered buckets, contradictory overlays, non-monotone haircuts, or eligibility that exceeds an agreement’s modeled constraints.

Why MLTTDB fits

Eligibility matrices are finite, structured, and rich in cross-field invariants. A proof model can type agreement scope and asset classifications, require complete bucket partitions, and express haircut monotonicity over an explicitly modeled risk order. MLTTDB can hold the approved rule rows and stress examples and revalidate them when a policy or agreement model changes. UUIDs make individual schedules traceable without implying that the store owns legal agreement truth.

Example architecture

agreement abstraction + security taxonomy + policy workbook
                        |
   external legal/risk mapping and reconciliation
                        v
      reviewed MLTTDB schedule workspace
                        |
   Agda finite-table or generated-definition validation
                        v
 native checker diagnostics + project-owned counterexample analysis
                        |
   collateral-engine compiler and golden test suite
                        v
    approval, activation, monitoring, dispute process

Legal and risk specialists first approve a structured abstraction of agreement terms. An adapter maps rule sources into typed candidates and reports classifications it cannot resolve. The proof source owns bucket and monotonicity definitions; MLTTDB stores reviewed schedules. Agda finite lookup is useful when later haircut rows reference earlier eligibility or classification rows. Lean and Rocq alternatives require their supported non-lookup preprocessor pattern. An external compiler builds engine-native configuration and is tested independently.

Representative typed artifacts

Useful types include Agreement, AssetClass, QualityBand, MaturityBucket, Eligibility agreement asset, Haircut agreement bucket, and ConcentrationOverlay. Tables might be eligibilityRules :T: EligibilityRule, baseHaircuts :T: HaircutRule, and stressCases :T: CollateralCase. A reconciled CollateralScheduleManifest aggregate term materializes the applicable taxonomy, buckets, precedence, and schedule rows for whole-snapshot checks. A haircut value can be a bounded percentage indexed by currency and bucket. The manifest may carry proof that worsening modeled quality or maturity does not reduce the base haircut, subject to explicitly represented policy exceptions.

Checks and evidence

For the compiler-reconciled schedule manifest, the checker can establish non-overlap or deliberate precedence of buckets, coverage of the manifest’s finite taxonomy, range validity, monotonic base-haircut relations, and agreement containment of eligibility rules. Representative cases can prove the expected abstract rule and overlay selection. Evidence should bind the result to agreement abstraction revision, taxonomy snapshot, manifest reconciliation, policy approval, mapping report, proof source, checker output, generated engine configuration digest, and golden-test outcomes. MLTTDB does not interpret contracts, classify a live security, price collateral, calculate exposure, validate market data, or execute substitutions and margin calls.

Potential benefits

Formal rule tables can expose holes and unintended inversions that are difficult to see in wide matrices. Rechecking identifies precisely which rows depend on a changed classification or agreement scope. The separation of formal predicates from reviewed terms supports controlled policy variation without copying fragile validation logic across workbooks and engines.

Deployment boundary

Position MLTTDB between policy/legal abstraction and engine configuration generation. Never use its success alone to determine collateral eligibility or valuation in production. Maintain external agreement governance, security-master reconciliation, maker-checker approval, independent calculation tests, monitoring, and dispute handling. Qualified legal, credit-risk, market-risk, collateral-operations, and quantitative reviewers must accept the mappings and assumptions.
04 Prudential and management reporting calculation-lineage dossier Explore pattern

Operational context

A finance and risk reporting function produces capital, liquidity, leverage, and internal management measures from governed data sets and calculation chains. A reported cell may depend on entity scope, portfolio classification, netting treatment, adjustments, aggregation, and sign conventions. Change review must show that each modeled output has an approved lineage path, compatible units, required adjustments, and a reconciliation disposition, without conflating structural correctness with the truth of reported numbers.

Why MLTTDB fits

Calculation lineage can be expressed as typed transformations between defined measures. Proof-assistant types can track unit, currency basis, reporting perimeter, and aggregation grain, while stored rows capture the current catalog of transformations and approved reconciliation cases. MLTTDB enables repeatable validation of this formal lineage as rules or mappings change. It is not a ledger, ETL platform, or numerical reporting engine.

Example architecture

data catalog + calculation repository + ledger/risk sources
                          |
      external lineage extractor and reconciler
                          v
      finance-owned MLTTDB lineage snapshot
                          |
    CI proof validation of graph and test cases
                          v
   typed-lineage evidence + generated definitions
                          |
   reporting engine tests and controlled close process
                          v
      attestations, submissions, and audit archive

The extractor derives candidate mappings from governed code and catalog metadata, preserves source pointers, and reports unparsed logic. Finance data owners review classification and perimeter. The formal repository defines abstract measure transformations. MLTTDB stores their reviewed instances and can be validated through Agda, Lean, or Rocq. Reporting engines, close orchestration, data-quality controls, attestations, and archival remain separate.

Representative typed artifacts

Types can include Measure unit perimeter grain, SourceCell measure, Transformation inputs output, Adjustment, Aggregation, and ReconciliationCase. Tables such as lineageSteps :T: LineageStep, reportingCells :T: ReportingCell, and reconciliations :T: ReconciliationCase hold row-level terms. A LineageManifest aggregate term, materialized and reconciled by the extractor, enumerates the nodes, edges, approved inputs, and declared outputs whose graph properties are checked. A transformation term can prove that input and output units align and that its entity perimeter is not silently widened. Numerical values used in representative cases are supplied snapshot data.

Checks and evidence

Over the reconciled lineage manifest, the proof assistant can reject unit or sign mismatches, cycles where the modeled calculation graph must be acyclic, missing inputs, invalid perimeter transitions, and reconciliation dispositions outside the approved taxonomy. It can establish structural reachability of each manifest output and correctness of small reference cases under the encoded calculation semantics. Evidence should include catalog and code revisions, source-data snapshot identifiers, extractor coverage and manifest reconciliation, term export, proof/checker versions, engine reconciliation tests, review comments, and attestation links. It does not guarantee ledger accuracy, data completeness, regulatory interpretation, numerical stability of a production engine, or timely filing.

Potential benefits

Reviewers can trace a changed definition through explicit typed dependencies and identify affected outputs before close. Unit and perimeter constraints catch classes of mapping defect earlier than end-stage variance analysis. A reproducible dossier connects rule intent, lineage declarations, checker evidence, and conventional reconciliations without pretending they are interchangeable.

Deployment boundary

Run MLTTDB as change-time and close-readiness assurance on frozen, identified snapshots. Keep authoritative calculations, adjustments, submissions, records retention, and attestations in controlled finance platforms. Reporting owners, accountants, regulatory specialists, model/risk experts, audit, and formal-methods reviewers must approve the semantics and evidence. A successful validation must never automatically release or submit a report.

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

Pre-trade risk control

About this workflow

This example represents the control gate between an order-management workflow and the venue or execution service. Its purpose is to answer a time-sensitive question in a reproducible way: may this order be released now, for this account and legal entity, against the firm’s current exposure and approved limits? The machine treats the decision as more than a single threshold check. It binds the order, positions, open orders, market data, limit hierarchy, and any authorized override into one traceable control outcome.

The straight-through path starts when an order is normalized and its account, product, venue, and timing context are captured. Current positions and open-order effects are then aggregated across the relevant risk boundaries. Product, desk, account, and entity constraints can be applied alongside a stress view using current market inputs. A passing order is released only with the control decision attached and only within its validity window. This matters because an exposure calculation can become stale between the original check and actual release.

The exception paths distinguish a genuine limit breach from an unreliable decision basis. Stale positions or market inputs send the case to risk recalculation; refreshed inputs return it to exposure aggregation, while a failed refresh results in rejection. A limit failure also produces a rejection, but an authorized user may request an exception review. Approval requires appropriate override authority, a documented rationale, and a bounded amount and expiry. A declined override remains rejected. Even after release, a material market change can invalidate the decision and force recalculation. An amended rejected order re-enters as a new order rather than inheriting an obsolete outcome.

These controls protect both speed and discipline. Traders receive a clear release or rejection, risk officers can see which constraint bound the decision, and control testing can reproduce the inputs and rule version used at the time. The explicit override route prevents informal workarounds while preserving a governed way to handle exceptional business circumstances.

Layer 1 — Pre-trade control lifecycle

This layer presents the end-to-end control outcome: receive an order, establish exposure, assess limits, release or reject, and resolve exceptional cases. It is the appropriate view for a head of trading, risk owner, or control assessor asking where the order is in the admission lifecycle and whether it followed an approved path. It intentionally omits individual data calls, aggregation calculations, and authorization checks.

Layer 2 — Risk decision operations

This layer shows the operating stages used by the trading and risk-control teams: normalization, exposure aggregation, limit evaluation, release, rejection, exception review, and recalculation. It includes the important loops for stale inputs, market changes, overrides, and amendments. It excludes the lowest-level mechanics of loading positions, evaluating each rule, or recording each approval attribute.

Layer 3 — Risk checks and actions

This layer exposes the executable control work inside each operation. It covers identifiers and order context, position and open-order loading, aggregation boundaries, entity and product limits, stress inputs, decision attachment, failure explanations, override authority, and refresh of stale data. It is suitable for control design and implementation review. It intentionally does not prescribe a particular risk engine, data schema, limit methodology, or venue protocol.
02

Regulatory reporting production

About this workflow

This example represents the controlled production of a regulatory return, from determining what must be reported through submission and evidence retention. It applies to recurring prudential, transaction, liquidity, capital, or statistical reporting where the exact form differs but the operating principles are consistent: use the right reporting entity, period, and rule version; source complete governed data; apply approved calculations; validate the result; and retain enough lineage to reproduce what was filed.

The main path begins by scoping the obligation and mapping each required field to its governed source. Reporting data is extracted and reconciled across position, transaction, reference-data, and ledger boundaries. Approved aggregation and valuation rules produce the reportable metrics, with intermediate results retained rather than overwritten. Validation then combines technical controls, such as schema and cross-field checks, with business review of material movements and threshold alerts. A validated report is transmitted through the authorized channel. The submission is not considered complete until its receipt and submission identity are captured, after which source lineage, approvals, and calculation evidence are packaged under the applicable retention and access rules.

Exception handling preserves the distinction between scope, source, calculation, validation, and transmission defects. A source-completeness gap returns to obligation scoping because the population or mapping may be wrong. A calculation exception or failed validation enters controlled correction and normally returns to metric calculation after the defect is fixed. If investigation changes the entity, period, population, or governing rule, it must be rescoped rather than patched downstream. A rejected transmission also enters correction, with the regulator’s response retained. Even after evidence has been archived, a restatement requirement reopens the correction path and preserves the relationship between the original filing and its replacement.

These controls matter because a plausible total is not necessarily a compliant report. Reviewers need to reproduce the population, rule version, transformations, judgments, approvals, and receipt. Explicit correction routes reduce the risk of silent spreadsheet adjustments, unsupported resubmissions, or evidence packages that no longer match the filed return.

Layer 1 — Regulatory report lifecycle

This layer communicates the reporting obligation’s overall progression: scope, assemble, calculate, validate, submit, retain, and correct when necessary. It is useful to the accountable executive, regulatory reporting owner, or audit team reviewing whether the filing reached an evidenced conclusion. It intentionally hides field-level transformations, individual validations, and channel-specific submission details.

Layer 2 — Reporting production operations

This layer shows the operational work performed by reporting, data, and finance-control teams. It distinguishes data assembly from calculation, validation from transmission, and correction from evidence retention. It includes loops for missing sources, calculation errors, validation failures, rejected submissions, rescoping, and restatement. It excludes the exact report taxonomy, regulator portal, and organizational approval matrix.

Layer 3 — Reporting checks and actions

This layer covers the concrete control actions: select entity, period, and rule version; map fields to sources; extract and reconcile records; apply aggregation and valuation rules; retain intermediates; run schema and cross-field controls; review movements; capture receipts; and package lineage and approvals. It supports procedure and automation design but intentionally does not encode a specific jurisdiction, return, accounting standard, calculation formula, or retention schedule.
03

Securities settlement control

About this workflow

This example models the post-trade control chain that takes a captured securities trade through matching, instruction, resource preparation, delivery-versus-payment, and books-and-records reconciliation. It is written from the perspective of settlement operations: a trade is not complete merely because execution occurred. The economics must agree with the counterparty, instructions must be eligible and accepted, cash and securities must be available, and final postings must reconcile with external market or custodian records.

The normal path begins by normalizing the trade economics, settlement parties, and source confirmations. Matching compares those terms with the counterparty and resolves permitted tolerances and standing settlement data. Once matched, synchronized instructions are sent to the relevant settlement infrastructure after validating market, account, and instrument eligibility. Operations then confirms that cash and securities are available and reserves them for the settlement window. Successful delivery-versus-payment establishes finality, after which positions, cash, and control evidence are posted.

The machine makes settlement breaks explicit rather than treating them as generic operational failures. A matching break returns the trade to capture so economics or static data can be corrected before instruction. An instruction rejection or resource shortfall opens settlement-fail management, where the reason and responsible party are classified under the applicable market practice. A recoverable fail can be reinstructed. A persistent fail moves to break reconciliation for comparison of internal records with the custodian, central securities depository, or agent. Reconciliation also follows an apparently completed settlement, because external finality and internal posting can disagree. A cleared break confirms completion; a posting defect routes back to instruction and controlled correction.

These controls matter for asset protection, liquidity management, client reporting, and regulatory obligations around settlement discipline. They prevent an unmatched or ineligible trade from consuming resources, make shortages visible before the settlement window closes, and ensure that “completed” means both market finality and accurate books and records. The retained evidence also supports fail ageing, counterparty claims, and operational-risk review.

Layer 1 — Securities settlement lifecycle

This layer shows the business outcome from captured trade to completed and reconciled settlement, including the possibility of a fail. It serves operations leadership, treasury, and control owners who need the overall status and the route taken. It deliberately leaves out instruction fields, reservation mechanics, matching tolerances, and individual reconciliation comparisons.

Layer 2 — Settlement operations

This layer identifies the operational work queues: trade capture, matching, instruction, resource readiness, completion, fail management, and break reconciliation. It includes the principal loops for match breaks, rejected instructions, shortages, retries, and posting corrections. It excludes detailed message formats, market deadlines, and the specific accounting entries used by a given firm.

Layer 3 — Settlement checks and actions

This layer describes the control activities performed within each queue: normalize economics, bind confirmations, compare counterparty terms, resolve tolerances, validate eligibility, send synchronized instructions, confirm and reserve resources, verify delivery-versus-payment finality, post balances, classify fails, and reconcile external and internal records. It is detailed enough for procedure design and system mapping while intentionally remaining neutral about asset class, market infrastructure, custodian, settlement cycle, and vendor platform.
Interactive state machine

Workflow demo

Skip to content

Domains

Finance

Placeholder domain page for financial rules involving risk limits, settlement, and reporting.

  • risk limits
  • settlement
  • reporting

Problems we solve

Checked boundaries and evidence

  • Risk limits combine positions, entities, products, and changing market conditions.
  • Settlement workflows depend on timing, eligibility, and exception handling.
  • Controls must remain consistent across data sources and reporting boundaries.
  • Reviewers need reproducible explanations for alerts and calculated outcomes.
Constraint Modeling

Represent limits, dependencies, and aggregation boundaries.

Limit Checking

Evaluate positions and events against approved constraints.

Exposure Simulation

Explore representative scenarios and threshold changes.

Settlement Validation

Check prerequisites, timing rules, and exception paths.

Reporting Evidence

Preserve traceable inputs and calculation decisions.

Application patterns

Imported product records

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

FF Scribe4 patterns
The Finance domain covers risk limits, settlement, and reporting across positions, legal entities, products, market conditions, timing, evidence, and system boundaries. These examples use FF Scribe to confirm precisely scoped financial propositions, not as a pricing engine, books-and-records platform, execution control, or source of financial truth. Each deployment needs an audited setup vocabulary and named authorities for limits, data, and decisions.
01Pre-trade risk-limit authorization

System/use case

A control workbench formalizes the decision rules used when an order is checked against counterparty, issuer, product, concentration, and desk mandates before release. It is most useful for explaining composite alerts and documenting what an approver means when requesting a new limit rule or an exception path.

Operational setting

Order and execution systems submit the account, legal entity, product taxonomy, direction, notional, and exposure snapshot. A risk service calculates approved metrics and identifies the applicable limits. Breaches, stale inputs, and classification conflicts enter a supervised risk queue; the trading desk may contribute, but approval remains independent.

Decision/claim boundary

The checked claim should express the logical boundary of authorization—for example, which reviewed facts imply escalation or release. It must not claim that an exposure number is accurate, that a market scenario is valid, or that a limit is commercially or regulatorily appropriate. The accountable risk function approves the setup vocabulary and the proposition; operations technology owns correct system enforcement.

Candidate checked statements

The following are illustrative controlled-English propositions for a future setup, not statements already implemented by FF Scribe:

  • For every order and applicable limit, if the projected exposure exceeds the approved limit, then the order requires independent risk approval.
  • For every order, if the position snapshot is stale, then automated release is inhibited.
  • For every approved exception, if its validity period has ended, then it does not authorize order release.

Example architecture

Order and reference-data events flow through a normalization layer to the existing exposure and limit engines. Those engines return metrics, limit identifiers, timestamps, and reason codes to a decision-orchestration service. FF Scribe sits beside the governed rule-authoring and review workflow: it receives a practitioner’s proposed meaning plus a versioned setup, not an unrestricted trading feed. The accepted type, readback candidate ID, setup version, compiler outcome, and user confirmation are stored in an immutable rule-review record. Enforcement remains in the independently tested pre-trade control service. A risk officer is the meaning and approval authority; neither the model nor the compiler can release an order.

Where verified readback fits

A risk specialist describes the intended authorization condition in natural language. The model proposes one setup-scoped proposition using only registered entities and relations. Agda checks that the expression is syntactically and type correct. If the separate partial readback stage supports its structure, it produces the finite audited family without model-authored paraphrase; unsupported structure fails visibly. The specialist accepts a successful reading or supplies feedback. That acceptance confirms intended meaning only; it is not a proof that a limit was breached or that the production control enforces the rule.

Potential benefits

  • Reduces ambiguity when desk, risk, and engineering teams translate a policy decision into a control specification.
  • Preserves a reproducible statement, vocabulary version, and reviewer confirmation for model-risk, internal-control, and change-governance evidence.
  • Makes hidden premises such as snapshot freshness, entity attribution, and exception validity visible before implementation.
  • Supports consistent review of alert reasons without allowing an LLM to invent the final confirmation wording.

Limits/adoption considerations

Type correctness establishes that a proposition is well formed in the chosen setup; it does not establish factual exposure, limit calibration, model validity, policy compliance, or control effectiveness. FF Scribe checks proposition types, not proof objects, so a checked implication is not proof that its premises or conclusion hold for a live order. Practitioner acceptance confirms the readback matches intended semantics, not that intent is authorized. Market-data lineage, metric reconciliation, independent model validation, access segregation, latency testing, and production surveillance remain separate controls.
02Securities settlement exception and release management

System/use case

A settlement-control application formalizes prerequisites and exception routes for delivery-versus-payment or receive-versus-payment instructions. It helps operations teams distinguish an unmatched instruction, an ineligible asset, missing inventory or cash, an invalid standing settlement instruction, and an approved hold or release.

Operational setting

Trade capture sends allocations and instructions to matching and settlement platforms. Custodian responses, inventory, cash projections, eligibility, calendars, and acknowledgements arrive asynchronously. Exceptions route to settlements operations, treasury, client service, or a control manager by reason and materiality. Existing venue and custodian adapters govern cut-off-sensitive actions.

Decision/claim boundary

The formalized proposition defines when a workflow may label an instruction ready, held, or escalated. It does not attest that securities or cash are available, that a custodian message is authentic, or that settlement finality has occurred. The settlement control owner approves rule meaning; operations staff remain accountable for exception disposition and any manual release.

Candidate checked statements

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

  • For every settlement instruction, if matching is confirmed and asset eligibility is confirmed, then the instruction is eligible for readiness review.
  • For every instruction, if the approved standing settlement instruction is absent, then automated release is inhibited.
  • For every settlement exception, if cash coverage is unresolved at the review cut-off, then the exception is escalated to the designated owner.

Example architecture

A canonical trade store correlates executions, allocations, and instruction versions. Event adapters ingest matching, custodian, depository, inventory, cash, and calendar status into a timestamped evidence ledger. A rules service computes operational status, while a case-management layer presents evidence and captures maker-checker actions. FF Scribe supports controlled rule review at configuration and change time. Accepted propositions and readbacks are linked to rule versions and test scenarios. The deterministic engine never sends settlement messages; authenticated adapters and dual-control workflows retain that capability. Human operators can reject stale or contradictory evidence and must record the basis of material overrides.

Where verified readback fits

An operations control designer states a proposed prerequisite or escalation rule in natural language. A model maps it to the finite vocabulary of the settlement setup. Agda type-checks the candidate. The partial readback translator then either renders supported structure through the deterministic audited family or reports unsupported structure without a partial reading. The designer explicitly accepts a successful reading or provides corrective feedback. This loop validates the shape and understood meaning of the proposition; it does not validate source messages, prove readiness, or authorize settlement.

Potential benefits

  • Produces reviewable rule specifications across operations, custody, treasury, and engineering terminology.
  • Makes exception classes and evidence prerequisites explicit, reducing conflation of “missing,” “failed,” “on hold,” and “not applicable.”
  • Links workflow changes to stable checked statements and human confirmations for regression design.
  • Improves post-incident reconstruction by preserving what reviewers believed a rule meant at a particular setup version.

Limits/adoption considerations

Temporal cut-offs, calendars, partial settlement, netting, finality, and venue-specific semantics need explicit modeling and cannot be inferred from ordinary language. A type-correct rule may still use stale or false facts, implement a poor operational policy, or disagree with a platform’s actual behavior. A checked proposition is not a completed proof of settlement eligibility. User confirmation is not maker-checker authorization. Reconciliation, message authentication, access control, resilience, and accountable manual decision-making remain mandatory.
03Financial and management reporting reconciliation

System/use case

A reporting-evidence service formalizes assertions around source-to-report reconciliation, adjustment approval, aggregation boundaries, and sign-off readiness. Typical users are financial controllers, product control, regulatory reporting operations, data owners, and internal audit.

Operational setting

Subledgers, the general ledger, valuation stores, counterparty masters, and governed data platforms feed a reporting mart. Reconciliation jobs compare balances and record breaks by source, account, entity, product, currency, and reporting period. Manual adjustments and mapping overrides pass through controlled journals and reviewer queues before report production.

Decision/claim boundary

The checked proposition should identify the evidence conditions for a reconciliation or sign-off state. It does not certify accounting treatment, valuation, completeness of source populations, control effectiveness, or the truth of a published report. The report owner and financial control authority decide whether evidence is sufficient and approve any attestation.

Candidate checked statements

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

  • For every report line and source balance, if the report line is mapped to the source balance and the reconciled variance is within the approved tolerance, then the line is eligible for controller review.
  • For every material break, if remediation evidence is absent, then period sign-off remains pending.
  • For every manual adjustment, if independent approval is recorded, then the adjustment is eligible for inclusion review.

Example architecture

Versioned connectors load extracts into a lineage catalog and reconciliation engine. Results, variances, mappings, tolerances, and data-quality flags enter an evidence store. A workflow assembles period sign-off packs with adjustment approvals and unresolved breaks. FF Scribe supports rule and attestation-template governance; each accepted proposition links to lineage, calculation version, control owner, and tests. Controllers decide sufficiency, and the tool cannot post journals or issue reports.

Where verified readback fits

A controller describes a readiness or escalation assertion. The model proposes a proposition limited to the reporting setup’s registered vocabulary. Agda checks the candidate type. For supported structure, audited deterministic readback produces the controlled finite family while preserving premise order and provenance; unsupported translation fails visibly. The controller accepts a successful reading or corrects it through feedback. The outcome is an intent-confirmed specification—not evidence that mappings are complete, balances agree, or a report is fairly presented.

Potential benefits

  • Creates a common, reproducible description of reconciliation and sign-off criteria across finance and data teams.
  • Exposes aggregation scope, tolerance, materiality, approval, and period dependencies that are often buried in prose or spreadsheets.
  • Provides stable inputs for test cases, control walkthroughs, and change-impact reviews.
  • Separates the model-generated candidate from compiler authority, deterministic readback, and controller acceptance.

Limits/adoption considerations

Accounting judgment, materiality, reporting perimeter, valuation methodology, and source completeness require accountable professional review. Type checking cannot establish factual truth or reporting compliance, and it does not test whether the implemented reconciliation behaves like the proposition. Proposition checking also does not complete a proof that sign-off conditions hold. Confirmation records user intent at that moment; it does not substitute for an authorized sign-off, control-performance evidence, or audit conclusion.
04Liquidity and collateral eligibility governance

System/use case

A treasury decision-support platform formalizes eligibility, concentration, haircut, substitution, and escalation statements used in collateral allocation and liquidity-buffer review. The aim is to make rule meaning reviewable before it is encoded in optimization and operational systems.

Operational setting

Inventory services supply security identifiers, ownership, encumbrance, location, and availability. Eligibility masters, agreements, limits, valuations, haircuts, and projected obligations feed an allocation engine. Treasury and collateral operations review shortfalls, substitutions, and disputed classifications; independent treasury risk owns limits and challenge.

Decision/claim boundary

A checked proposition can express conditions under which an asset is eligible for allocation review or a shortfall requires escalation. It does not prove title, asset availability, valuation accuracy, legal enforceability, optimal allocation, or adequate liquidity. Treasury risk and the designated collateral authority remain accountable for classifications, limits, and overrides.

Candidate checked statements

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

  • For every asset and obligation, if the asset satisfies the approved eligibility class and remains unencumbered, then it is eligible for allocation review.
  • For every collateral pool, if the projected concentration exceeds the approved threshold, then the pool requires treasury-risk review.
  • For every proposed substitution, if equivalent coverage is not established, then release of the original collateral is inhibited.

Example architecture

A governed reference-data layer normalizes asset, counterparty, agreement, and eligibility identifiers. Valuation, haircut, inventory, concentration, and optimization services publish versioned results with timestamps and data lineage. An orchestration layer creates review cases and retains pre- and post-decision snapshots. FF Scribe supports the policy-to-rule review path, and its accepted proposition, deterministic readback, setup hash, and practitioner response become part of the rule’s approval package. Allocation execution remains behind existing entitlements, dual control, and downstream confirmation; humans adjudicate conflicting agreements or data.

Where verified readback fits

A treasury specialist states the intended eligibility or escalation rule in natural language. A model proposes a setup-scoped Agda type, and Agda checks type correctness. If the partial readback implementation supports that structure, it returns the deterministic finite family; otherwise the workflow fails visibly. The specialist explicitly accepts a successful reading or gives feedback for revision. No step demonstrates that the asset satisfies the premises, proves adequacy, or confirms that the optimizer used the rule.

Potential benefits

  • Aligns treasury, legal, risk, operations, and engineering on precise eligibility and exception semantics.
  • Preserves traceable rule intent across agreement, reference-data, and optimization changes.
  • Makes human override and escalation boundaries explicit before automation.
  • Supplies stable propositions for scenario design and implementation conformance testing.

Limits/adoption considerations

Agreement interpretation, legal enforceability, liquidity stress assumptions, haircut suitability, and optimization quality are outside type checking. Real-time availability and valuation remain factual inputs requiring independent controls. A well-typed proposition is neither a proof that coverage exists nor evidence that the production process is effective. Practitioner confirmation establishes understood intent only; formal rule approval and allocation authority must remain segregated, authenticated, and auditable.
MLTTDB4 patterns
These illustrative applications develop the Finance domain brief in ~/nn-ff-web/content/domains/finance.md: constraint modeling, limit checking, exposure scenarios, settlement validation, and traceable reporting evidence. They propose assurance components, not trading, risk, settlement, accounting, or regulatory systems. Relevant business owners, quantitative specialists, operations professionals, counsel, auditors, and formal-methods reviewers must approve the financial interpretation and the encoded models.
01Pre-trade limit rule release assurance

Operational context

An institutional trading platform maintains pre-trade rules for counterparty, issuer, product, desk, concentration, tenor, and mandate limits. Production engines combine positions, orders, reference data, prices, netting sets, and intraday utilization under strict latency constraints. Before a rule package is promoted, market-risk and technology teams need evidence that aggregation scopes are well-formed, limit precedence is unambiguous, exception routes are explicit, and representative boundary scenarios produce results consistent with the approved policy model.

Why MLTTDB fits

The release artifact is a finite catalog of limit definitions, scope relations, and scenario witnesses. Proof-assistant types can distinguish currencies, products, legal entities, and aggregation levels while encoding invariants such as scope containment and threshold ordering. MLTTDB can hold reviewed rule instances and boundary cases separately from the formal model, then rerun them as definitions change. It is appropriate for offline assurance, not low-latency order admission.

Example architecture

limit inventory + mandate system + risk taxonomy
                     |
     external rule compiler and reconciler
                     v
       MLTTDB candidate release catalog
                     |
        project-owned CI validation
                     v
          proof-assistant checker
                     |
 checked scenarios + executable-engine test vectors
                     v
   risk approval and production rule deployment

The compiler maps authoritative limit records into reviewed proof-language terms, retains source identifiers, and reports omissions or ambiguous taxonomies. A formal-policy repository defines scopes, precedence, and scenario semantics. The term store preserves catalog order and UUIDs. CI runs the proof checker plus parity tests against the actual pre-trade engine. A separate deployment service enforces entitlements, approvals, effective times, and rollback.

Representative typed artifacts

Candidate types include LegalEntity, TradingBook, RiskFactor, AggregationScope, Limit scope measure, Utilization measure, and BoundaryCase. Tables could be approvedScopes :T: AggregationScope, limitRules :T: LimitRule, and releaseCases :T: BoundaryCase. A compiler-reconciled LimitReleaseManifest aggregate term enumerates the scopes, precedence relations, limit rules, exceptions, and boundary-case UUIDs used for release-wide checks. A concentration limit term can carry proof that its child scopes are contained in the parent mandate and that warning thresholds do not exceed the hard limit. Scenario terms use supplied, normalized quantities rather than querying live positions or prices.

Checks and evidence

The checker can reject inconsistent units, orphan scopes, duplicate precedence for the same modeled condition, a soft threshold above a hard threshold, or an exception class not permitted for a mandate. It can prove expected classifications for zero, just-below, at-limit, and just-above boundary cases under the abstract semantics. Evidence should bind the typed snapshot to source inventory versions, transformation report, proof revision, checker output, production-engine build, and parity-test results. MLTTDB does not establish current utilization, valuation accuracy, booking completeness, market-data quality, or runtime engine behavior.

Potential benefits

Risk and engineering teams get an explicit, reviewable rule semantics rather than relying exclusively on configuration diffing. Type distinctions reduce category and unit errors, while reusable boundary proofs improve regression coverage when aggregation taxonomies or precedence change. Stable row identifiers help link limits, approvals, incidents, and model changes.

Deployment boundary

Run MLTTDB in the rule-authoring and release pipeline, isolated from the synchronous order path. A passing result is one input to approval, never an authorization to trade or deploy. Production kill switches, independent controls, entitlements, observability, reconciliation, and rollback remain mandatory. Qualified risk owners and formal reviewers must validate the abstraction, and engine parity must be demonstrated separately.
02Settlement instruction and lifecycle rule validation

Operational context

A securities operations function maintains standing settlement instructions and lifecycle rules across legal entities, accounts, custodians, markets, instruments, settlement methods, and currencies. Misaligned account ownership, invalid market/currency combinations, or unclear instruction precedence can cause repair queues and settlement failure. Operations teams need a controlled way to validate proposed reference-data changes and modeled instruction selection before activation.

Why MLTTDB fits

Instruction eligibility and precedence can be represented as a finite typed relation: an instruction is valid only for a declared party, account, market, asset class, method, and effective-status input. MLTTDB can store reviewed reference terms and test cases and use a proof assistant to establish uniqueness or explicit ambiguity handling under the modeled selection rules. Explicit priority and specificity fields in an aggregate instruction manifest carry preference semantics; the store’s stable order supplies deterministic presentation and generated-definition emission only.

Example architecture

SSI master + security master + account/custodian records
                        |
      external reconciliation and candidate adapter
                        v
    operations four-eyes review in staging workspace
                        |
          MLTTDB instruction catalog
                        |
      store-orchestrated proof verification
                        v
     consistency report + downstream test fixture
                        |
   reference-data activation and settlement platform

Authoritative masters remain outside MLTTDB. The adapter resolves identifiers, proposes terms, and produces unmatched-record and effective-date reports. Operations reviewers confirm candidates. The term store can launch the configured backend, but the checker supplies semantic success or diagnostics. Activation, maker-checker approvals, message generation, sanctions controls, and settlement processing remain with existing platforms.

Representative typed artifacts

Types might include Party, SafekeepingAccount party, CashAccount party currency, Market, InstrumentClass, SettlementMethod, InstructionScope, and StandingInstruction scope. Tables such as accounts :T: AccountBinding, instructions :T: SettlementInstruction, and selectionCases :T: SelectionCase can express ownership and admissible combinations. An InstructionSelectionManifest aggregate term, built by the reference-data adapter and reconciled to the master-data and row exports, materializes scopes, explicit priorities, accounts, instructions, and representative cases for whole-snapshot checks. In Agda, an instruction row can refer to an earlier approved account by UUID finite lookup. In Lean or Rocq, relationships must use ordinary generated definitions or be embedded in supported row structures.

Checks and evidence

Validation can ensure that modeled cash and safekeeping accounts belong to the declared entity, selected currencies and markets are permitted, preference ranks are unique within an overlapping scope, fallback is explicit, and every supplied representative case resolves to exactly one instruction or a deliberately modeled exception. The release packet should include master-data snapshot IDs, adapter reconciliation, reviewed MLTTDB export, proof model and checker versions, diagnostics, downstream message-schema tests, and approval record. The proof does not authenticate instructions, determine real-time eligibility, screen parties, predict settlement, or verify an external custodian’s acceptance.

Potential benefits

Typed staging can catch referential and scope errors before instructions enter high-volume processing. Explicit selection proofs clarify why a representative trade selects a particular instruction and make precedence changes easier to regression-test. Persistent UUIDs provide durable linkage between catalog entries, repair incidents, and review decisions.

Deployment boundary

Use this as pre-activation reference-data assurance, never as the live settlement instruction resolver unless a separately engineered and validated runtime implements the approved semantics. Restrict catalog administration through external IAM and dual control. Operations, treasury, legal, compliance, and custodian-management specialists must review applicable fields, and independent reconciliations must confirm that activated downstream records match the approved snapshot.
03Collateral eligibility and haircut configuration

Operational context

A collateral management function configures eligibility schedules and haircuts by agreement, counterparty, issuer, asset class, rating band, currency, maturity bucket, concentration tier, and liquidity characteristics. The operational engine consumes positions and valuations, while policy teams approve rule matrices and overlays. Configuration changes risk creating uncovered buckets, contradictory overlays, non-monotone haircuts, or eligibility that exceeds an agreement’s modeled constraints.

Why MLTTDB fits

Eligibility matrices are finite, structured, and rich in cross-field invariants. A proof model can type agreement scope and asset classifications, require complete bucket partitions, and express haircut monotonicity over an explicitly modeled risk order. MLTTDB can hold the approved rule rows and stress examples and revalidate them when a policy or agreement model changes. UUIDs make individual schedules traceable without implying that the store owns legal agreement truth.

Example architecture

agreement abstraction + security taxonomy + policy workbook
                        |
   external legal/risk mapping and reconciliation
                        v
      reviewed MLTTDB schedule workspace
                        |
   Agda finite-table or generated-definition validation
                        v
 native checker diagnostics + project-owned counterexample analysis
                        |
   collateral-engine compiler and golden test suite
                        v
    approval, activation, monitoring, dispute process

Legal and risk specialists first approve a structured abstraction of agreement terms. An adapter maps rule sources into typed candidates and reports classifications it cannot resolve. The proof source owns bucket and monotonicity definitions; MLTTDB stores reviewed schedules. Agda finite lookup is useful when later haircut rows reference earlier eligibility or classification rows. Lean and Rocq alternatives require their supported non-lookup preprocessor pattern. An external compiler builds engine-native configuration and is tested independently.

Representative typed artifacts

Useful types include Agreement, AssetClass, QualityBand, MaturityBucket, Eligibility agreement asset, Haircut agreement bucket, and ConcentrationOverlay. Tables might be eligibilityRules :T: EligibilityRule, baseHaircuts :T: HaircutRule, and stressCases :T: CollateralCase. A reconciled CollateralScheduleManifest aggregate term materializes the applicable taxonomy, buckets, precedence, and schedule rows for whole-snapshot checks. A haircut value can be a bounded percentage indexed by currency and bucket. The manifest may carry proof that worsening modeled quality or maturity does not reduce the base haircut, subject to explicitly represented policy exceptions.

Checks and evidence

For the compiler-reconciled schedule manifest, the checker can establish non-overlap or deliberate precedence of buckets, coverage of the manifest’s finite taxonomy, range validity, monotonic base-haircut relations, and agreement containment of eligibility rules. Representative cases can prove the expected abstract rule and overlay selection. Evidence should bind the result to agreement abstraction revision, taxonomy snapshot, manifest reconciliation, policy approval, mapping report, proof source, checker output, generated engine configuration digest, and golden-test outcomes. MLTTDB does not interpret contracts, classify a live security, price collateral, calculate exposure, validate market data, or execute substitutions and margin calls.

Potential benefits

Formal rule tables can expose holes and unintended inversions that are difficult to see in wide matrices. Rechecking identifies precisely which rows depend on a changed classification or agreement scope. The separation of formal predicates from reviewed terms supports controlled policy variation without copying fragile validation logic across workbooks and engines.

Deployment boundary

Position MLTTDB between policy/legal abstraction and engine configuration generation. Never use its success alone to determine collateral eligibility or valuation in production. Maintain external agreement governance, security-master reconciliation, maker-checker approval, independent calculation tests, monitoring, and dispute handling. Qualified legal, credit-risk, market-risk, collateral-operations, and quantitative reviewers must accept the mappings and assumptions.
04Prudential and management reporting calculation-lineage dossier

Operational context

A finance and risk reporting function produces capital, liquidity, leverage, and internal management measures from governed data sets and calculation chains. A reported cell may depend on entity scope, portfolio classification, netting treatment, adjustments, aggregation, and sign conventions. Change review must show that each modeled output has an approved lineage path, compatible units, required adjustments, and a reconciliation disposition, without conflating structural correctness with the truth of reported numbers.

Why MLTTDB fits

Calculation lineage can be expressed as typed transformations between defined measures. Proof-assistant types can track unit, currency basis, reporting perimeter, and aggregation grain, while stored rows capture the current catalog of transformations and approved reconciliation cases. MLTTDB enables repeatable validation of this formal lineage as rules or mappings change. It is not a ledger, ETL platform, or numerical reporting engine.

Example architecture

data catalog + calculation repository + ledger/risk sources
                          |
      external lineage extractor and reconciler
                          v
      finance-owned MLTTDB lineage snapshot
                          |
    CI proof validation of graph and test cases
                          v
   typed-lineage evidence + generated definitions
                          |
   reporting engine tests and controlled close process
                          v
      attestations, submissions, and audit archive

The extractor derives candidate mappings from governed code and catalog metadata, preserves source pointers, and reports unparsed logic. Finance data owners review classification and perimeter. The formal repository defines abstract measure transformations. MLTTDB stores their reviewed instances and can be validated through Agda, Lean, or Rocq. Reporting engines, close orchestration, data-quality controls, attestations, and archival remain separate.

Representative typed artifacts

Types can include Measure unit perimeter grain, SourceCell measure, Transformation inputs output, Adjustment, Aggregation, and ReconciliationCase. Tables such as lineageSteps :T: LineageStep, reportingCells :T: ReportingCell, and reconciliations :T: ReconciliationCase hold row-level terms. A LineageManifest aggregate term, materialized and reconciled by the extractor, enumerates the nodes, edges, approved inputs, and declared outputs whose graph properties are checked. A transformation term can prove that input and output units align and that its entity perimeter is not silently widened. Numerical values used in representative cases are supplied snapshot data.

Checks and evidence

Over the reconciled lineage manifest, the proof assistant can reject unit or sign mismatches, cycles where the modeled calculation graph must be acyclic, missing inputs, invalid perimeter transitions, and reconciliation dispositions outside the approved taxonomy. It can establish structural reachability of each manifest output and correctness of small reference cases under the encoded calculation semantics. Evidence should include catalog and code revisions, source-data snapshot identifiers, extractor coverage and manifest reconciliation, term export, proof/checker versions, engine reconciliation tests, review comments, and attestation links. It does not guarantee ledger accuracy, data completeness, regulatory interpretation, numerical stability of a production engine, or timely filing.

Potential benefits

Reviewers can trace a changed definition through explicit typed dependencies and identify affected outputs before close. Unit and perimeter constraints catch classes of mapping defect earlier than end-stage variance analysis. A reproducible dossier connects rule intent, lineage declarations, checker evidence, and conventional reconciliations without pretending they are interchangeable.

Deployment boundary

Run MLTTDB as change-time and close-readiness assurance on frozen, identified snapshots. Keep authoritative calculations, adjustments, submissions, records retention, and attestations in controlled finance platforms. Reporting owners, accountants, regulatory specialists, model/risk experts, audit, and formal-methods reviewers must approve the semantics and evidence. A successful validation must never automatically release or submit a report.
State Machine Studio3 demos
SMPre-trade risk control

This example represents the control gate between an order-management workflow and the venue or execution service. Its purpose is to answer a time-sensitive question in a reproducible way: may this order be released now, for this account and legal entity, against the firm’s current exposure and approved limits? The machine treats the decision as more than a single threshold check. It binds the order, positions, open orders, market data, limit hierarchy, and any authorized override into one traceable control outcome.

The straight-through path starts when an order is normalized and its account, product, venue, and timing context are captured. Current positions and open-order effects are then aggregated across the relevant risk boundaries. Product, desk, account, and entity constraints can be applied alongside a stress view using current market inputs. A passing order is released only with the control decision attached and only within its validity window. This matters because an exposure calculation can become stale between the original check and actual release.

The exception paths distinguish a genuine limit breach from an unreliable decision basis. Stale positions or market inputs send the case to risk recalculation; refreshed inputs return it to exposure aggregation, while a failed refresh results in rejection. A limit failure also produces a rejection, but an authorized user may request an exception review. Approval requires appropriate override authority, a documented rationale, and a bounded amount and expiry. A declined override remains rejected. Even after release, a material market change can invalidate the decision and force recalculation. An amended rejected order re-enters as a new order rather than inheriting an obsolete outcome.

These controls protect both speed and discipline. Traders receive a clear release or rejection, risk officers can see which constraint bound the decision, and control testing can reproduce the inputs and rule version used at the time. The explicit override route prevents informal workarounds while preserving a governed way to handle exceptional business circumstances.

Layer 1 — Pre-trade control lifecycle

This layer presents the end-to-end control outcome: receive an order, establish exposure, assess limits, release or reject, and resolve exceptional cases. It is the appropriate view for a head of trading, risk owner, or control assessor asking where the order is in the admission lifecycle and whether it followed an approved path. It intentionally omits individual data calls, aggregation calculations, and authorization checks.

Layer 2 — Risk decision operations

This layer shows the operating stages used by the trading and risk-control teams: normalization, exposure aggregation, limit evaluation, release, rejection, exception review, and recalculation. It includes the important loops for stale inputs, market changes, overrides, and amendments. It excludes the lowest-level mechanics of loading positions, evaluating each rule, or recording each approval attribute.

Layer 3 — Risk checks and actions

This layer exposes the executable control work inside each operation. It covers identifiers and order context, position and open-order loading, aggregation boundaries, entity and product limits, stress inputs, decision attachment, failure explanations, override authority, and refresh of stale data. It is suitable for control design and implementation review. It intentionally does not prescribe a particular risk engine, data schema, limit methodology, or venue protocol.
Open interactive model
SMRegulatory reporting production

This example represents the controlled production of a regulatory return, from determining what must be reported through submission and evidence retention. It applies to recurring prudential, transaction, liquidity, capital, or statistical reporting where the exact form differs but the operating principles are consistent: use the right reporting entity, period, and rule version; source complete governed data; apply approved calculations; validate the result; and retain enough lineage to reproduce what was filed.

The main path begins by scoping the obligation and mapping each required field to its governed source. Reporting data is extracted and reconciled across position, transaction, reference-data, and ledger boundaries. Approved aggregation and valuation rules produce the reportable metrics, with intermediate results retained rather than overwritten. Validation then combines technical controls, such as schema and cross-field checks, with business review of material movements and threshold alerts. A validated report is transmitted through the authorized channel. The submission is not considered complete until its receipt and submission identity are captured, after which source lineage, approvals, and calculation evidence are packaged under the applicable retention and access rules.

Exception handling preserves the distinction between scope, source, calculation, validation, and transmission defects. A source-completeness gap returns to obligation scoping because the population or mapping may be wrong. A calculation exception or failed validation enters controlled correction and normally returns to metric calculation after the defect is fixed. If investigation changes the entity, period, population, or governing rule, it must be rescoped rather than patched downstream. A rejected transmission also enters correction, with the regulator’s response retained. Even after evidence has been archived, a restatement requirement reopens the correction path and preserves the relationship between the original filing and its replacement.

These controls matter because a plausible total is not necessarily a compliant report. Reviewers need to reproduce the population, rule version, transformations, judgments, approvals, and receipt. Explicit correction routes reduce the risk of silent spreadsheet adjustments, unsupported resubmissions, or evidence packages that no longer match the filed return.

Layer 1 — Regulatory report lifecycle

This layer communicates the reporting obligation’s overall progression: scope, assemble, calculate, validate, submit, retain, and correct when necessary. It is useful to the accountable executive, regulatory reporting owner, or audit team reviewing whether the filing reached an evidenced conclusion. It intentionally hides field-level transformations, individual validations, and channel-specific submission details.

Layer 2 — Reporting production operations

This layer shows the operational work performed by reporting, data, and finance-control teams. It distinguishes data assembly from calculation, validation from transmission, and correction from evidence retention. It includes loops for missing sources, calculation errors, validation failures, rejected submissions, rescoping, and restatement. It excludes the exact report taxonomy, regulator portal, and organizational approval matrix.

Layer 3 — Reporting checks and actions

This layer covers the concrete control actions: select entity, period, and rule version; map fields to sources; extract and reconcile records; apply aggregation and valuation rules; retain intermediates; run schema and cross-field controls; review movements; capture receipts; and package lineage and approvals. It supports procedure and automation design but intentionally does not encode a specific jurisdiction, return, accounting standard, calculation formula, or retention schedule.
Open interactive model
SMSecurities settlement control

This example models the post-trade control chain that takes a captured securities trade through matching, instruction, resource preparation, delivery-versus-payment, and books-and-records reconciliation. It is written from the perspective of settlement operations: a trade is not complete merely because execution occurred. The economics must agree with the counterparty, instructions must be eligible and accepted, cash and securities must be available, and final postings must reconcile with external market or custodian records.

The normal path begins by normalizing the trade economics, settlement parties, and source confirmations. Matching compares those terms with the counterparty and resolves permitted tolerances and standing settlement data. Once matched, synchronized instructions are sent to the relevant settlement infrastructure after validating market, account, and instrument eligibility. Operations then confirms that cash and securities are available and reserves them for the settlement window. Successful delivery-versus-payment establishes finality, after which positions, cash, and control evidence are posted.

The machine makes settlement breaks explicit rather than treating them as generic operational failures. A matching break returns the trade to capture so economics or static data can be corrected before instruction. An instruction rejection or resource shortfall opens settlement-fail management, where the reason and responsible party are classified under the applicable market practice. A recoverable fail can be reinstructed. A persistent fail moves to break reconciliation for comparison of internal records with the custodian, central securities depository, or agent. Reconciliation also follows an apparently completed settlement, because external finality and internal posting can disagree. A cleared break confirms completion; a posting defect routes back to instruction and controlled correction.

These controls matter for asset protection, liquidity management, client reporting, and regulatory obligations around settlement discipline. They prevent an unmatched or ineligible trade from consuming resources, make shortages visible before the settlement window closes, and ensure that “completed” means both market finality and accurate books and records. The retained evidence also supports fail ageing, counterparty claims, and operational-risk review.

Layer 1 — Securities settlement lifecycle

This layer shows the business outcome from captured trade to completed and reconciled settlement, including the possibility of a fail. It serves operations leadership, treasury, and control owners who need the overall status and the route taken. It deliberately leaves out instruction fields, reservation mechanics, matching tolerances, and individual reconciliation comparisons.

Layer 2 — Settlement operations

This layer identifies the operational work queues: trade capture, matching, instruction, resource readiness, completion, fail management, and break reconciliation. It includes the principal loops for match breaks, rejected instructions, shortages, retries, and posting corrections. It excludes detailed message formats, market deadlines, and the specific accounting entries used by a given firm.

Layer 3 — Settlement checks and actions

This layer describes the control activities performed within each queue: normalize economics, bind confirmations, compare counterparty terms, resolve tolerances, validate eligibility, send synchronized instructions, confirm and reserve resources, verify delivery-versus-payment finality, post balances, classify fails, and reconcile external and internal records. It is detailed enough for procedure design and system mapping while intentionally remaining neutral about asset class, market infrastructure, custodian, settlement cycle, and vendor platform.
Open interactive model
Explore patternsReview product applications

Cabinet index

Explore Formal Foundry

Search the archive

Find a page

Type to search the published content.