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.
01 Pre-trade risk-limit authorization Explore pattern
System/use case
Operational setting
Decision/claim boundary
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
Where verified readback fits
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
02 Securities settlement exception and release management Explore pattern
System/use case
Operational setting
Decision/claim boundary
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
Where verified readback fits
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
03 Financial and management reporting reconciliation Explore pattern
System/use case
Operational setting
Decision/claim boundary
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
Where verified readback fits
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
04 Liquidity and collateral eligibility governance Explore pattern
System/use case
Operational setting
Decision/claim boundary
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
Where verified readback fits
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
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
Why MLTTDB fits
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
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
Potential benefits
Deployment boundary
02 Settlement instruction and lifecycle rule validation Explore pattern
Operational context
Why MLTTDB fits
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
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
Potential benefits
Deployment boundary
03 Collateral eligibility and haircut configuration Explore pattern
Operational context
Why MLTTDB fits
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
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
Potential benefits
Deployment boundary
04 Prudential and management reporting calculation-lineage dossier Explore pattern
Operational context
Why MLTTDB fits
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
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
Potential benefits
Deployment boundary
These read-only, pan-and-zoom models expose three abstraction levels for each workflow. They are explanatory examples, not live operational or decision systems.
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
Layer 2 — Risk decision operations
Layer 3 — Risk checks and actions
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
Layer 2 — Reporting production operations
Layer 3 — Reporting checks and actions
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.