×

Policy

Challenges

  • Policy intent must become precise operational criteria and decision steps.
  • Eligibility thresholds interact with exceptions, evidence, and appeal routes.
  • Small wording changes can produce broad downstream implementation effects.
  • Stakeholders need explanations that connect outcomes back to approved policy.

Problems We Solve

  • Policy Representation Structure definitions, criteria, exceptions, and dependencies.
  • Eligibility Validation Check decisions against explicit qualifying conditions.
  • Impact Simulation Compare representative outcomes before policy changes.
  • Consistency Checking Find gaps between policy intent and operating rules.
  • Decision Explanation Present a traceable path from inputs to outcome.

Domain portfolio

Application patterns

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

The Policy domain covers eligibility, thresholds, exceptions, evidence, appeals, and translating public-policy intent into operational rules. These applications make a policy owner’s proposed rule structure inspectable before adoption or use. They support validation, impact comparison, consistency, and explanation; they do not confer eligibility, establish case facts, determine lawful authority, or replace accountable governance.
01 Public-benefit eligibility determination workbench Explore pattern

System/use case

A caseworker-facing workbench helps a benefits program express qualifying conditions, disqualifiers, household or applicant attributes, evidence requirements, and exception routes as controlled propositions. It is intended to improve the meaning review of rules used in intake and adjudication, while keeping actual determinations within the program’s authorized case process.

Operational setting

The workbench integrates with intake, identity and evidence services, case management, and a versioned policy manual. A policy owner selects the program, population, period, and approved setup. Caseworkers see provenance and mark inputs as verified, alleged, missing, inconsistent, or under review. Supervisors control exceptions; appeals remain appropriately independent.

Decision/claim boundary

The candidate proposition can express, for example, that satisfying an approved set of qualifying conditions and having no applicable exclusion entails an eligibility classification. Type checking only validates that the proposition uses the setup’s concepts coherently. It does not verify applicant data, determine whether evidence is sufficient, prove that the policy is lawful, compute a payment, or authorize an adverse action. The designated policy owner controls rule meaning, and an authorized decision-maker remains responsible for each determination.

Candidate checked statements

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

  • “For every applicant, if the qualifying threshold is met and required residency evidence is verified, the applicant is eligible for substantive review.”
  • “If a mandatory evidence item is missing, the case requires evidence follow-up rather than an eligibility denial.”
  • “Every adverse preliminary outcome has an available supervisor-review route.”

These are examples of candidate statements, not claims that current setups implement these predicates or that any applicant satisfies them.

Example architecture

A policy registry stores rule versions, definitions, periods, and exception ownership. Case systems provide normalized attributes with provenance. An orchestration service selects the setup pinned to the case period and sends the practitioner’s formulation to FF Scribe. The checked type, readback family, setup, sources, and disposition enter a protected record. A separate engine may apply only propositions promoted through governance. Formalization review stays distinct from live adjudication and high-impact decisions remain human.

Where verified readback fits

A policy analyst or authorized casework lead describes the intended eligibility relationship in natural language. The model proposes one setup-scoped proposition or asks for clarification. Agda checks whether the type is well formed under the curated vocabulary. If the partial readback translator supports its structure, ff-readback deterministically renders the finite audited family without model-authored paraphrase; unsupported structure fails visibly. The author accepts whether a successful reading captures the intended statement or gives corrective feedback. Agda acceptance is not proof of eligibility or factual truth, and a policy owner separately authorizes rule use; the program’s authorized process still makes the case decision.

Potential benefits

The workbench can reduce divergent interpretations and help reviewers notice omitted exceptions or distinguish incomplete evidence from substantive failure; FF Scribe does not perform those completeness checks automatically. Stable readbacks improve training, review, and handoffs. Versioned records show which approved criteria a process was designed to apply without opaque model recommendations.

Limits/adoption considerations

Public benefits involve hardship provisions, evidentiary judgment, accessibility duties, and procedural protections that resist binary encoding. Programs need user testing, language access, bias and impact review, data minimization, contestability, and a manual path for unsupported cases. Threshold calculations and source validation require separate testing. Policy and legal review precede production.
02 Policy-to-operations rule traceability service Explore pattern

System/use case

A traceability service helps a public body or regulated program translate approved policy text into operating procedures, form questions, service rules, staff guidance, and software requirements. It gives policy owners a controlled way to state dependencies and then inspect exactly what formal structure was checked.

Operational setting

The service supports implementation and change management using approved instruments, intent notes, definitions, process models, forms, and rule inventories. Policy, legal, service-design, operations, and technology owners retain layer-specific sign-off. Every setup has a named source version and owner.

Decision/claim boundary

A checked statement can describe the intended relationship between policy conditions and an operational step, such as referral, evidence collection, or supervisory review. It does not prove that the procedure faithfully or completely implements the policy, that the source is legally valid, that the associated software behaves correctly, or that frontline practice follows the procedure. These broader assurance claims need evidence, testing, and accountable review beyond type checking.

Candidate checked statements

Possible illustrative candidates are:

  • “If an application enters the exceptional-circumstances route, standard automatic disposition is inhibited.”
  • “Every operational eligibility rule must reference an approved policy criterion.”
  • “If a policy criterion changes, each dependent form question and decision step requires owner review.”

Example architecture

A repository maintains policy clauses, rationale, and implementation artifacts. A dependency graph connects criteria to procedures, fields, notices, controls, and software. Policy owners use FF Scribe to confirm setup-bounded dependency statements. Validation detects unowned or stale edges; conventional tests verify application behavior. Accepted readbacks link change requests to checked types and sources. Normal legal, policy, security, accessibility, and operational gates control deployment.

Where verified readback fits

An implementation owner states a desired policy-to-process relationship. The model maps that request to a candidate type using the setup’s approved entities and predicates. Agda determines whether the formal composition is valid, not whether the relationship is substantively justified. For a supported translation, the deterministic readback family exposes what was actually checked; unsupported structure fails visibly. The implementation owner can confirm whether that reading captures the authored statement, while a policy owner separately approves or rejects its substantive use. Neither action is proof completion, source interpretation, implementation testing, or confirmation that downstream components honor the proposition.

Potential benefits

The service can reveal orphaned rules, trace small wording changes, and reduce gaps among policy, guidance, forms, and software. Reviewers can challenge a precise proposition instead of inferring behavior from code. Dependencies support regression planning and ownership.

Limits/adoption considerations

Traceability is only as complete as the maintained inventory. Policy rationales, discretionary judgments, and service-design considerations may not fit a proposition vocabulary and should remain first-class narrative artifacts. Organizations need setup review boards, semantic versioning, deprecation procedures, controlled source ingestion, and clear responsibility for each edge. Formal checks complement but do not replace policy conformity assessment, user research, accessibility testing, or software verification.
03 Proposed-policy scenario and distributional-review sandbox Explore pattern

System/use case

A scenario sandbox allows analysts to compare how alternative policy formulations classify representative cases before a proposal is approved. Verified readback makes each scenario assertion reviewable, so discussion can separate the chosen rule structure from empirical forecasts and value judgments.

Operational setting

The sandbox supports option appraisal and implementation planning. Teams define baseline and proposed setups, synthetic cases, thresholds, and exceptions. A separate environment holds administrative data, microsimulation models, costing assumptions, and uncertainty ranges. Stakeholders can inspect formal readings without sensitive records.

Decision/claim boundary

The checked proposition states how a curated policy setup relates case features to a classification or process step. It does not establish causal impact, predict behavior, prove fiscal estimates, show distributional fairness, or determine that a scenario represents the population. Agda type correctness cannot validate parameter values or data. Policy owners authorize the rule interpretation; economists, statisticians, equality specialists, affected communities, and decision-makers remain responsible for their respective assessments.

Candidate checked statements

Illustrative candidates include:

  • “Under option B, every household meeting the revised threshold enters the qualifying cohort unless an approved exclusion applies.”
  • “If a representative case qualifies under the baseline but not the proposal, that case is classified as a transition loss.”
  • “Every scenario with an unresolved exception requires qualitative policy review.”

Example architecture

A registry versions cases, parameters, and provenance. FF Scribe checks propositions under baseline and candidate setups and retains readbacks. An evaluator applies approved propositions to synthetic or governed data. Microsimulation and costing consume classifications with explicit model versions and assumptions. A dashboard joins rule deltas to aggregate outcomes and impact evidence. Promotion requires policy authority and established decision processes.

Where verified readback fits

The analyst describes an expected rule or comparison in domain language. The model proposes a setup-limited Agda type, and the compiler checks its structural validity. If the partial readback stage supports that structure, ff-readback renders the audited candidates; otherwise it fails visibly. The analyst confirms whether a successful reading captures the proposed statement, and the policy owner separately authorizes the option’s interpretation or use. This records what rule was posed to the scenario engine; it neither proves the proposition from empirical data nor endorses the proposal. Factual validity, parameter authority, representativeness, and policy legitimacy remain independent review questions.

Potential benefits

Teams can compare options against stable, inspectable rule statements and detect where a changed threshold or exception alters classification. The separation of formal rule, scenario data, and simulation assumptions improves reproducibility and helps prevent a generated explanation from obscuring a modeling choice. It can also focus stakeholder review on cases where formalization is unsupported or transition treatment is unclear.

Limits/adoption considerations

Scenario outputs can create false precision when behavioral responses, take-up, administrative capacity, or data coverage are uncertain. Representative cases must be governed and complemented by empirical and participatory analysis. Setups need explicit effective periods and parameter provenance. The interface should show uncertainty, unsupported cases, and differences between rule classification and modeled outcome, with no automatic policy ranking or deployment.
04 Appeals, reconsideration, and decision-explanation quality service Explore pattern

System/use case

A quality service checks whether proposed decision explanations and reconsideration routes reflect an approved policy structure. It helps case reviewers ensure that an outcome references relevant criteria, identifies missing evidence appropriately, and exposes available review paths without allowing generative text to invent a rationale.

Operational setting

The service operates before notice issuance or during reconsideration. It receives proposition identifiers, evidence statuses, policy version, reason codes, and route status. Personal information and documents stay in the case system. Independent reviewers see the checked rule and readbacks alongside the complete record.

Decision/claim boundary

The tool may check a proposition that certain recorded premises entail a program-defined outcome or review step. It does not decide disputed facts, assess witness credibility, validate an explanation as legally sufficient, or determine an appeal. It also does not prove that all relevant reasons were included. Authorized caseworkers, supervisors, hearing officers, tribunals, or courts retain their established responsibilities.

Candidate checked statements

Future controlled vocabularies might support candidates such as:

  • “If the only unmet condition is supported by evidence under review, the case remains pending rather than finally adverse.”
  • “Every adverse decision explanation identifies the applicable criterion and the recorded case finding.”
  • “If a reviewer overturns the original classification, the case requires a revised notice and decision record.”

Example architecture

The case system supplies findings and evidence status; a registry supplies criteria and reasons. FF Scribe checks propositions during authoring and controlled review. An explanation assembler uses accepted readbacks plus approved facts and templates. Quality checks flag absent criteria or inconsistent routes. Event records preserve determinations, setup versions, and reviewer actions. Authorized approval and accessibility standards govern notices.

Where verified readback fits

A policy owner or appeal specialist expresses the intended relation among a finding, disposition, and review route. The model forms a candidate in the relevant setup, and Agda checks its type. Supported structure yields the deterministic audited readback family; unsupported translation fails visibly. The author confirms whether a successful reading captures the intended statement or provides feedback, while the authorized policy or appeals role separately approves its use. The wording can anchor an explanation template, but it does not confirm real-world facts, demonstrate that a burden has been met, or validate the final notice. Meaning confirmation and adjudicative authority remain separate.

Potential benefits

The service can improve consistency of reason structures, reduce explanations that cite the wrong policy version, and make reconsideration transitions more traceable. It supports quality sampling by showing which checked rule and case findings underlay a draft disposition. Clear separation between missing evidence, a failed criterion, and an exception route may also improve procedural fairness and reduce avoidable appeals.

Limits/adoption considerations

Good explanations require context, plain-language and accessibility expertise, and often individualized reasoning beyond a finite readback. The service should never generate unreviewed adverse notices or suppress inconvenient evidence. Programs need independent appeals safeguards, record-correction mechanisms, bias monitoring, language access, retention controls, and transparent accountability. Audited readbacks must be revalidated whenever policy vocabulary or reason-code mappings change.

Applicability frame

MLTTDB can support policy assurance when an approved policy has been translated into proof-assistant row types, tables, and propositions. Agda, Lean, or Rocq source owns that semantic model. The SQLite store owns ordered source-language rows, UUIDs, projections, language metadata, and stored table definitions; it can start verification, but the proof assistant performs the semantic check. Agda currently supports finite lookup of known UUID rows subject to declaration and dependency rules. Current Lean and Rocq preprocessors do not support that lookup. Consultation, source-data stewardship, identity and access, case workflow, evidence assessment, system reconciliation, operational decisions, runtime enforcement, provenance, and formalization governance must be supplied by surrounding components.

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 impact, 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 policy review.

01 Public-benefit eligibility operations assurance Explore pattern

Operational context

A public agency or delegated administrator operates a benefit with categorical, household, income, residency, contribution, and exception criteria. Caseworkers collect evidence and make findings in a case-management system, while a policy operations team maintains procedure manuals and decision reason codes. The assurance need is to identify structurally incomplete or internally inconsistent proposed decisions before issuance and to test whether an approved operational rule set faithfully covers the policy’s modeled paths. It is not a replacement for caseworker judgment, evidence assessment, or appeal rights.

Why MLTTDB fits

Policy specialists can encode evidence statuses, household roles, threshold bands, qualifying conditions, exceptions, and outcome categories as distinct types rather than loosely coupled fields. A case projection then becomes an ordered, reviewable proof-assistant term. Propositions can require that an approval cites a complete qualifying path, that an adverse result exposes the failed condition and available review route, and that Unknown or disputed inputs lead to referral rather than being treated as false. Separating source declarations from stored scenarios also supports regression when a threshold or exception changes.

Example architecture

case system -> worker-confirmed findings -> minimal case projection adapter
policy instrument -> accountable formalization -> model repository
projection -> MLTTDB -> Agda/Lean/Rocq check -> supervisor queue -> case workflow

The case platform retains personal data, evidence, correspondence, and final authority. A privacy-minimizing adapter maps reviewed findings to the formal vocabulary and writes source-language rows. CI or the store launches the verifier against a pinned model. A result translator presents failed proof obligations and model assumptions to a supervisor. Only the external case workflow records approval, produces notice content, triggers payment, and manages reconsideration or appeal.

Representative typed artifacts

Declarations might include policyVersions :T: PolicyVersion, householdScenarios :T: HouseholdScenario, and decisionProposals :T: DecisionProposal. Types distinguish Submitted, Verified, Disputed, and Unavailable evidence and use an explicit ThreeWay result such as Qualifies, DoesNotQualify, or NeedsReview. Threshold values carry unit, household basis, period, and effective interval. A proposition such as supportedDecision connects only confirmed modeled findings to a proposed reason path. In Agda, proposals may look up earlier policy-version rows by UUID; portable models should avoid assuming the same capability in Lean or Rocq.

Checks and evidence

Schema mode checks a revised vocabulary before migration. Data mode rejects ill-typed projections, out-of-period policy references, missing reason routes, and attempts to use unresolved evidence as confirmed. Synthetic boundary suites cover values just below, at, and above thresholds; household transitions; exceptions; and incomplete evidence. External evidence records retain the model commit, policy approval identifier, ordered row UUIDs, source-case revision, verifier output, supervisor disposition, and notice revision. Sampling reconciles projections to the source file and tests explanation accessibility.

Potential benefits

The operation can catch incomplete reason paths earlier, make policy assumptions visible to supervisors, and distinguish genuinely adverse results from cases needing more evidence. Typed threshold units reduce common translation errors. Regression suites reveal which representative households change outcome under an approved amendment, while stable UUIDs let policy and delivery teams discuss the same cases. The result is better assurance evidence, not a claim of mechanically correct entitlement.

Deployment boundary

MLTTDB does not authenticate applicants, establish residency or income, assess credibility, interpret the governing instrument, decide eligibility, issue notices, make payment, detect fraud, or decide appeals. It does not guarantee fairness or legal compliance. Production use requires authorized decision-makers, privacy and security controls, accessibility, bias and equality review, explanation and challenge routes, source reconciliation, monitoring, and fail-safe manual processing. Policy owners and qualified legal reviewers approve all rules and release decisions.
02 Grant-program award-criteria validation Explore pattern

Operational context

A grant-making body runs competitive programs with gateway eligibility, eligible-cost rules, strategic priorities, scoring rubrics, portfolio constraints, conflicts procedures, and delegated approval limits. Program officers and independent assessors work in a grants platform. Before a call opens, the policy team needs assurance that application forms, rubric configurations, and decision reason codes align with the approved scheme; before an award panel, it needs a consistency check on proposed decision packets without automating merit judgment.

Why MLTTDB fits

Formal types can keep gateway criteria separate from scored merit, advisory indicators, and portfolio-level considerations. This prevents an implementation from accidentally treating a high score as curing failed eligibility or treating an optional priority as mandatory. Typed rows can capture assessor-confirmed rubric selections, declared conflicts, moderation status, and proposed recommendations. Proof obligations can require complete scoring dimensions, valid delegation, explicit treatment of applicable exclusions, and a permissible reason code for each recommendation state.

Example architecture

approved scheme -> policy-to-model review -> versioned proof model
grant platform configuration -> configuration exporter -> MLTTDB assurance database
assessor packets -> batch verification -> exception dashboard -> panel secretariat

The proof model is developed and approved before program configuration. An exporter renders the actual grant-platform configuration and selected de-identified assessor packets into typed source terms, rather than maintaining an unconnected duplicate. A batch service fetches the ordered tables and runs proof-assistant validation. The exception dashboard groups failures by criterion or model proposition. The secretariat resolves discrepancies in the authoritative grants system and records panel and delegated decisions there.

Representative typed artifacts

Candidate tables include programCalls :T: ProgramCall, rubricDefinitions :T: RubricDefinition, assessmentPackets :T: AssessmentPacket, and delegations :T: Delegation. A Criterion records whether it is gateway, scored, tie-break, or advisory, plus evidence requirement and effective call. AssessmentPacket distinguishes raw assessor judgments from moderated values and the panel recommendation. A GrantConfigurationManifest aggregate term, reconciled to the platform export, enumerates the questions, reason codes, rubric criteria, and delegations used for whole-configuration checks. Propositions can then check that weights belong to the approved rubric, all mandatory dimensions represented in the manifest have dispositions, conflicted assessors do not supply counted scores, and the proposed approving role has sufficient delegation. Cross-row lookup can be concise in Agda; other backends need generated or embedded associations.

Checks and evidence

Pre-opening checks compare every configured question and reason code with its formal criterion and reject orphaned or duplicated mappings. Pre-panel checks validate packet completeness, score ranges, declared weighting arithmetic, moderation state, and delegation. Scenario fixtures include consortia, conditional awards, partial eligible costs, conflicts, tied rankings, and insufficient budgets. Evidence combines approved scheme and rubric identifiers, platform-configuration export hash, model revision, ordered UUIDs, checker transcript, exception resolutions, and panel approval record. A separate audit samples source assessments and access logs.

Potential benefits

Configuration errors can be found before applicants encounter them. Panels receive cleaner packets and a transparent separation between mechanical gateway checks and human merit judgments. Program changes become regression-testable, and delegation or conflict rules are less likely to be applied inconsistently. The retained validation evidence can support internal assurance and lessons learned without displacing the formal award record.

Deployment boundary

MLTTDB does not assess proposal quality, verify applicant assertions, manage conflicts, rank a portfolio, optimize a budget, award funds, or establish lawful authority. It is not a substitute for panel deliberation, procurement or subsidy-control analysis, financial due diligence, equality assessment, or legal review. Identity, documents, scoring workflow, audit logs, notifications, payments, and appeals remain external. Accountable officials approve the model and every funding decision.
03 Permit and licence decision-table preflight Explore pattern

Operational context

A regulator or local authority administers several permit and licence classes. Each class has scope conditions, mandatory documents, fitness or technical findings, consultation steps, statutory or policy timeframes, conditions, renewals, and referral routes. Legacy workflow configurations often reproduce the same rules differently across channels. The proposed preflight service checks the decision table and a proposed application disposition for coherence before a designated officer acts; it does not create an automatic right to grant or refuse.

Why MLTTDB fits

A proof-assistant model can express permit class, activity scope, applicant role, evidence state, mandatory consultation, officer delegation, possible conditions, and terminal disposition as typed alternatives. Tables can hold reviewed rule profiles and synthetic or actual case projections. Propositions can require every in-scope application to reach either a permitted decision state or an explicit referral, prohibit conditions that are unavailable for the selected class, and prevent an expired evidence item from satisfying a modeled currency requirement. Unknown facts remain explicit instead of becoming default negatives.

Example architecture

policy and authority sources -> multidisciplinary rule workshop -> proof model
online portal/case system -> reconciliation adapter -> MLTTDB typed projection
officer preflight -> proof-assistant result -> reasoned human decision -> register

Policy, legal, operational, and subject-matter specialists jointly approve the model. The portal and case system remain authoritative for applications, evidence, fees, consultations, and correspondence. A reconciliation adapter creates a minimal projection with source revision identifiers. Verification may be initiated from the officer workbench through store orchestration, but semantic errors come from Agda, Lean, or Rocq. A decision service blocks release only according to separately approved workflow policy and records the officer’s independent disposition in the authoritative register.

Representative typed artifacts

The source might declare licenceClasses :T: LicenceClass, decisionProfiles :T: DecisionProfile, applicationProjections :T: ApplicationProjection, and conditionSets :T: ConditionSet. EvidenceStatus distinguishes received, validated, disputed, waived-with-authority, and expired. DecisionProfile associates mandatory findings and consultation paths with one effective policy version. A PermitConfigurationManifest aggregate term, built from and reconciled to the portal configuration export, enumerates routes, classes, evidence and reason codes, delegations, and condition templates. Decision procedures may compute proofs or counterexample data, but presenting that data requires a project-owned evaluator and result encoder; store-owned row evaluation is currently Agda-only. An Agda implementation can refer to earlier class and condition rows via literal UUID lookups; Lean/Rocq preprocessors require ordinary generated associations.

Checks and evidence

Configuration assurance checks the reconciled manifest: every enumerated portal route maps to one modeled class, required evidence codes are reachable, reason codes correspond to allowed outcomes, delegations are current in the modeled snapshot, and condition templates match class and decision. Case preflight checks completeness and consistency of the confirmed projection. Boundary fixtures cover renewals, changes of control, multiple activities, consultation objections, waiver authority, expiry, and manual referral. Evidence records the model and configuration revisions, manifest reconciliation, ordered UUIDs, source-case revision, verifier output, officer resolution, and final register entry in an external audit service.

Potential benefits

The authority can reduce channel-specific rule drift, uncover unreachable or contradictory configuration before deployment, and present officers with focused missing-input or incompatible-condition findings. Explicit referral states make uncertainty safer. Synthetic scenario suites improve communication between policy designers and delivery teams, while stable formal artifacts make changes easier to review across permit classes.

Deployment boundary

MLTTDB does not validate documents, inspect premises, assess fitness, resolve objections, determine jurisdiction, grant or revoke a licence, publish a register, or enforce conditions. It provides neither legal authority nor a complete administrative record. The surrounding system needs identity checks, payments, evidence custody, consultation, officer delegation, procedural fairness, accessibility, reasons, review and appeal, security, and manual continuity. Qualified policy, legal, and technical reviewers approve both formal rules and operational deployment.
04 Policy-change impact and regression laboratory Explore pattern

Operational context

A central policy team is considering amendments to thresholds, definitions, exception routes, or transition provisions for an existing program. Analysts need to compare the current and proposed operational formalizations across a governed scenario library, understand which paths change, and identify implementation gaps before public consultation or rollout. Conventional spreadsheets are useful for costing but often hide classification assumptions and cannot demonstrate that all modeled cases reach a defined state.

Why MLTTDB fits

MLTTDB can hold ordered, stable scenario terms while separate proof-model branches encode current and candidate policies. The proof assistant can check scenario well-formedness and properties of the classification functions, such as exhaustiveness over a deliberately finite modeled domain, mutual exclusion of outcome constructors, or explicit NeedsReview handling. Running the same UUID-addressed scenarios against both branches yields a precise semantic regression set. This complements, rather than replaces, economic models and qualitative policy analysis.

Example architecture

research and consultation -> policy hypotheses -> current/candidate model branches
governed scenarios + declared paths/witnesses -> MLTTDB -> dual verification runs
checked declarations -> project-owned comparator -> impact review portal and teams

A scenario governance group approves synthetic archetypes, boundary cases, and any privacy-protected samples. Model authors encode proposals with traceable links to policy design decisions. For portability, each branch-specific scenario declaration carries a declared PolicyPath and a witness under that branch’s decision relation. A runner validates those declarations; a project-owned comparator then groups changed, unchanged, newly indeterminate, and invalid declarations and links them to assumptions. It does not treat generic validation output as a computed classification API. Costing, distributional analysis, operational design, and consultation use those findings as one input and remain separate systems and disciplines.

Representative typed artifacts

Tables could include scenarioCohorts :T: ScenarioCohort, policyScenarios :T: PolicyScenario, and expectedTransitions :T: ExpectedTransition. A scenario records units, time basis, evidence status, and explicitly bounded characteristics, never a loose map of fields. Each ExpectedTransition names a model branch, declares an algebraic PolicyPath and modeled reasons, and carries a witness that the branch’s decision relation admits that path. Propositions check total handling of the selected finite domain, transition-rule applicability, and preservation requirements identified by policy owners. In Agda, earlier-table UUID lookups can share cohort definitions; for backend portability, scenarios can be generated as self-contained terms.

Checks and evidence

The laboratory checks each branch’s declared paths and witnesses independently before the project-owned comparator compares those checked declarations. Regression gates flag changed paths, modeled reasons, required evidence, transition handling, and new proof failures. Metamorphic cases vary one modeled characteristic at a time to expose unexpected discontinuities; threshold fixtures cover boundary and unit conversions. Review evidence includes both commits, the scenario snapshot and ordered UUIDs, checker logs, comparison algorithm version, approved expected-change list, and reviewer dispositions. Statistical representativeness and fiscal estimates are validated by their own methods.

Potential benefits

Policy teams gain a concrete map from proposed wording and formal assumptions to representative operational effects. Unexpected changes can be discussed before implementation, and intended changes become explicit regression expectations. Reusable scenario identities improve collaboration among policy, legal, digital, and operations specialists. Formal checks can reveal gaps or contradictions that sensitivity tables alone miss.

Deployment boundary

MLTTDB does not forecast behavior, estimate expenditure, establish causal impact, determine distributional fairness, run consultation, interpret source law, or approve policy. Scenario coverage does not guarantee population coverage, and a proof is only about the formal model and supplied terms. Production decisions require empirical analysis, equality and rights assessment, legal review, stakeholder participation, privacy governance, implementation testing, and accountable authorization. The laboratory must clearly label assumptions and never present illustrative outputs as official entitlements.

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

Emergency relief delivery

About this workflow

This example represents delivery of time-critical public assistance after a disaster or emergency while preserving eligibility, authorization, delivery, and reconciliation controls. It recognizes the central operational tension: a program must act quickly enough to meet immediate safety and subsistence needs, yet still prevent duplicate, diverted, or unsupported payments and retain a reviewable explanation of who received what assistance.

The workflow starts by capturing the immediate need and contact details and assigning a traceable relief case. Urgency triage evaluates safety and the time available to act, then selects standard or expedited handling under published criteria. Standard cases proceed through event, location, and household verification. Missing evidence can return the request to intake for completion. In an expedited case, emergency evidence exceptions are documented and authorization may occur before the normal evidentiary package is complete; expedited handling changes the sequence, not the obligation to account for the decision.

Authorization calculates the permitted assistance package and approves the delivery channel and its controls. Delivery dispatches funds, goods, or services and confirms recipient access. A failed, duplicate, or diverted delivery opens an exception and protects remaining value while staff investigate. A corrected exception can resume delivery, while a conflict in entitlement, amount, or channel returns for reauthorization. Confirmed delivery advances to reconciliation, where the case team compares authorization with delivery records and publishes a reviewable outcome. A later reconciliation gap reopens the exception rather than being written off as administratively complete.

These controls matter because emergency conditions weaken ordinary evidence sources, displace households, create urgency, and attract fraud attempts at the same time. A traceable case identifier and explicit expedited criteria support equitable triage. Bounded authorization and delivery controls limit loss without delaying every case. Reconciliation allows the program to act on provisional evidence while preserving accountability to affected people, program managers, finance teams, and public auditors.

Layer 1 — Emergency relief lifecycle

This layer gives incident leadership the end-to-end status of relief cases: received, triaged, verified, authorized, delivering, reconciled, or in exception. It makes the expedited route and recovery loops visible across the program. It deliberately excludes specific identity checks, payment instructions, and delivery confirmations so leaders can assess reach, bottlenecks, and control exposure during the event.

Layer 2 — Relief case operations

This is the coordination view for intake teams, eligibility staff, authorizers, delivery partners, and reconciliation staff. It covers triage categories, verification standards, emergency exceptions, benefit calculation, channel approval, dispatch, failed-delivery handling, reauthorization, and closeout reconciliation. It includes ownership and handoffs but excludes each system field, document query, or payment API call.

Layer 3 — Relief checks and actions

This layer contains case-level execution: capture needs, check event and location, document a waived or deferred item, calculate the permitted package, issue funds or goods, confirm access, detect duplicates, protect unspent value, and reconcile authorization to delivery. It provides a reproducible decision and disbursement trail while leaving event-wide policy choices and lifecycle posture to the higher layers.
02

Housing assistance determination

About this workflow

This example represents a public housing-support determination from application through evidence review, eligibility decision, payment authorization, renewal, material-change review, denial, and appeal. It treats eligibility as a reasoned case decision rather than a single income comparison: household composition, residence, housing cost, need thresholds, evidence rules, exceptions, and the applicable policy period all contribute to the outcome.

The workflow starts by registering the household application and issuing clear evidence and consent requirements. Case staff verify household, residence, and cost records and resolve omissions or inconsistent declarations. Incomplete evidence returns to intake so the applicant can respond instead of producing an unexplained adverse decision. Once the record is complete, the eligibility decision applies income and need thresholds, records any authorized exception, and produces an explanation tied to the relied-upon criteria.

An eligible household moves to active assistance, where the payment schedule is authorized and renewal and change-reporting obligations are monitored. A household that does not meet the criteria receives reasons and an open reconsideration window. A timely appeal assembles the original decision record and routes new evidence to independent review; review can uphold the denial or reverse it and activate assistance. Active cases are not assumed to remain static. A reported material change pauses payments only under the applicable rule and triggers review. Cleared changes restore assistance, disqualifying changes produce a reasoned denial, and scheduled renewals return the case to evidence review.

These controls matter because small factual or policy differences can affect access to essential housing support. Clear evidence requests reduce avoidable attrition, a recorded rule path supports consistent decisions across caseworkers, and independent appeal prevents the original conclusion from becoming self-validating. Renewal and change controls protect public funds while ensuring that suspension or denial follows an authorized process and remains explainable to the household, supervisors, auditors, and review bodies.

Layer 1 — Housing assistance lifecycle

This layer is the program and case-status view: received, under evidence review, decided, active, denied, appealed, or suspended. It shows the full route to assistance and the safeguards around adverse or changed decisions. It intentionally excludes document-level verification, calculation fields, and payment-system commands so policy owners can see throughput, fairness checkpoints, and unresolved case posture.

Layer 2 — Eligibility case operations

This is the operational view for caseworkers, supervisors, appeal officers, and payment administrators. It covers evidence requests, verification, threshold application, decision notices, reconsideration windows, independent review, renewal, material-change handling, and restoration or denial. It includes handoffs and decision authority but excludes individual database updates and field-by-field evidence checks.

Layer 3 — Decision checks and actions

This layer contains the concrete case actions: register the household, verify residence and housing cost, resolve declarations, calculate relevant income and need, record exceptions, issue reasons, assemble the appeal record, authorize a schedule, and pause or restore payment. It supports an auditable decision trace while leaving policy-wide performance and lifecycle status to the higher layers.
03

Public grant administration

About this workflow

This example represents a competitive public-grant program from publication of the funding opportunity through eligibility screening, merit assessment, award, performance monitoring, remediation, and closeout. It connects the approved policy objectives and assessment criteria to award decisions, milestone payments, outcome evidence, expenditure review, and the retained public record.

The workflow begins when the authority publishes objectives, thresholds, exclusions, submission rules, and a controlled clarification record. After the submission window closes, applications are screened for timeliness and applicant eligibility. Curable defects return through the published clarification or correction route; non-curable conditions are recorded consistently. Eligible proposals proceed to assessment against the approved criteria, with conflicts of interest and moderation evidence captured. An inconsistency can reopen screening rather than allowing an unreliable score to advance.

An approved proposal becomes an active award with executed conditions and funding released only against authorized milestones. Monitoring reviews outcome and expenditure evidence and applies defined variance and change-control thresholds. Completed milestones and satisfactory final records permit closeout. Non-performance, an award-condition breach, or a closeout gap enters remediation. The response may be a corrective plan followed by renewed monitoring, reissued award terms, suspension, or recovery action. Even a nominally closed grant can reopen if final financial or outcome evidence does not support closure.

These controls matter because public funding decisions must be fair, consistent, and demonstrably connected to published purposes. Controlled clarifications avoid giving one applicant an informational advantage. Eligibility screening and conflict management protect the integrity of competition, while moderated scoring makes judgment reviewable without pretending it is mechanical. Milestone controls, documented variations, and remediation protect public money and program outcomes. A retained decision and audit trail supports applicants, oversight bodies, auditors, and the public in understanding both selection and post-award stewardship.

Layer 1 — Public grant lifecycle

This layer is the portfolio and governance view: opportunity published, applications screened, proposals assessed, award active, performance monitored, grant closed, or remediation underway. It shows the main accountability gates from appropriation intent to closeout. It intentionally excludes individual score entries, invoice checks, and payment operations so program leaders can see competition status, award health, and unresolved exposure.

Layer 2 — Grant administration operations

This is the working view for program officers, assessment panels, grants finance, contract managers, and assurance staff. It covers publication and clarifications, eligibility screening, scoring and moderation, conflict handling, award conditions, milestone releases, variation control, monitoring, remediation, recovery, and closeout. It includes the operational decision points but excludes atomic document and system actions.

Layer 3 — Grant checks and actions

This layer contains the evidence-bearing tasks: test submission and applicant eligibility, record defects, score criteria, declare conflicts, retain moderation reasons, execute conditions, validate milestone and expenditure evidence, apply variance thresholds, issue corrective actions, and reconcile final records. It is detailed enough to audit a decision or payment while leaving program-wide policy and lifecycle posture to the higher layers.
Interactive state machine

Workflow demo
Skip to content

Domains

Policy

Placeholder domain page for policy rules involving eligibility, thresholds, and public systems.

  • eligibility
  • thresholds
  • public systems

Problems we solve

Checked boundaries and evidence

  • Policy intent must become precise operational criteria and decision steps.
  • Eligibility thresholds interact with exceptions, evidence, and appeal routes.
  • Small wording changes can produce broad downstream implementation effects.
  • Stakeholders need explanations that connect outcomes back to approved policy.
Policy Representation

Structure definitions, criteria, exceptions, and dependencies.

Eligibility Validation

Check decisions against explicit qualifying conditions.

Impact Simulation

Compare representative outcomes before policy changes.

Consistency Checking

Find gaps between policy intent and operating rules.

Decision Explanation

Present a traceable path from inputs to outcome.

Application patterns

Imported product records

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

FF Scribe4 patterns
The Policy domain covers eligibility, thresholds, exceptions, evidence, appeals, and translating public-policy intent into operational rules. These applications make a policy owner’s proposed rule structure inspectable before adoption or use. They support validation, impact comparison, consistency, and explanation; they do not confer eligibility, establish case facts, determine lawful authority, or replace accountable governance.
01Public-benefit eligibility determination workbench

System/use case

A caseworker-facing workbench helps a benefits program express qualifying conditions, disqualifiers, household or applicant attributes, evidence requirements, and exception routes as controlled propositions. It is intended to improve the meaning review of rules used in intake and adjudication, while keeping actual determinations within the program’s authorized case process.

Operational setting

The workbench integrates with intake, identity and evidence services, case management, and a versioned policy manual. A policy owner selects the program, population, period, and approved setup. Caseworkers see provenance and mark inputs as verified, alleged, missing, inconsistent, or under review. Supervisors control exceptions; appeals remain appropriately independent.

Decision/claim boundary

The candidate proposition can express, for example, that satisfying an approved set of qualifying conditions and having no applicable exclusion entails an eligibility classification. Type checking only validates that the proposition uses the setup’s concepts coherently. It does not verify applicant data, determine whether evidence is sufficient, prove that the policy is lawful, compute a payment, or authorize an adverse action. The designated policy owner controls rule meaning, and an authorized decision-maker remains responsible for each determination.

Candidate checked statements

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

  • “For every applicant, if the qualifying threshold is met and required residency evidence is verified, the applicant is eligible for substantive review.”
  • “If a mandatory evidence item is missing, the case requires evidence follow-up rather than an eligibility denial.”
  • “Every adverse preliminary outcome has an available supervisor-review route.”

These are examples of candidate statements, not claims that current setups implement these predicates or that any applicant satisfies them.

Example architecture

A policy registry stores rule versions, definitions, periods, and exception ownership. Case systems provide normalized attributes with provenance. An orchestration service selects the setup pinned to the case period and sends the practitioner’s formulation to FF Scribe. The checked type, readback family, setup, sources, and disposition enter a protected record. A separate engine may apply only propositions promoted through governance. Formalization review stays distinct from live adjudication and high-impact decisions remain human.

Where verified readback fits

A policy analyst or authorized casework lead describes the intended eligibility relationship in natural language. The model proposes one setup-scoped proposition or asks for clarification. Agda checks whether the type is well formed under the curated vocabulary. If the partial readback translator supports its structure, ff-readback deterministically renders the finite audited family without model-authored paraphrase; unsupported structure fails visibly. The author accepts whether a successful reading captures the intended statement or gives corrective feedback. Agda acceptance is not proof of eligibility or factual truth, and a policy owner separately authorizes rule use; the program’s authorized process still makes the case decision.

Potential benefits

The workbench can reduce divergent interpretations and help reviewers notice omitted exceptions or distinguish incomplete evidence from substantive failure; FF Scribe does not perform those completeness checks automatically. Stable readbacks improve training, review, and handoffs. Versioned records show which approved criteria a process was designed to apply without opaque model recommendations.

Limits/adoption considerations

Public benefits involve hardship provisions, evidentiary judgment, accessibility duties, and procedural protections that resist binary encoding. Programs need user testing, language access, bias and impact review, data minimization, contestability, and a manual path for unsupported cases. Threshold calculations and source validation require separate testing. Policy and legal review precede production.
02Policy-to-operations rule traceability service

System/use case

A traceability service helps a public body or regulated program translate approved policy text into operating procedures, form questions, service rules, staff guidance, and software requirements. It gives policy owners a controlled way to state dependencies and then inspect exactly what formal structure was checked.

Operational setting

The service supports implementation and change management using approved instruments, intent notes, definitions, process models, forms, and rule inventories. Policy, legal, service-design, operations, and technology owners retain layer-specific sign-off. Every setup has a named source version and owner.

Decision/claim boundary

A checked statement can describe the intended relationship between policy conditions and an operational step, such as referral, evidence collection, or supervisory review. It does not prove that the procedure faithfully or completely implements the policy, that the source is legally valid, that the associated software behaves correctly, or that frontline practice follows the procedure. These broader assurance claims need evidence, testing, and accountable review beyond type checking.

Candidate checked statements

Possible illustrative candidates are:

  • “If an application enters the exceptional-circumstances route, standard automatic disposition is inhibited.”
  • “Every operational eligibility rule must reference an approved policy criterion.”
  • “If a policy criterion changes, each dependent form question and decision step requires owner review.”

Example architecture

A repository maintains policy clauses, rationale, and implementation artifacts. A dependency graph connects criteria to procedures, fields, notices, controls, and software. Policy owners use FF Scribe to confirm setup-bounded dependency statements. Validation detects unowned or stale edges; conventional tests verify application behavior. Accepted readbacks link change requests to checked types and sources. Normal legal, policy, security, accessibility, and operational gates control deployment.

Where verified readback fits

An implementation owner states a desired policy-to-process relationship. The model maps that request to a candidate type using the setup’s approved entities and predicates. Agda determines whether the formal composition is valid, not whether the relationship is substantively justified. For a supported translation, the deterministic readback family exposes what was actually checked; unsupported structure fails visibly. The implementation owner can confirm whether that reading captures the authored statement, while a policy owner separately approves or rejects its substantive use. Neither action is proof completion, source interpretation, implementation testing, or confirmation that downstream components honor the proposition.

Potential benefits

The service can reveal orphaned rules, trace small wording changes, and reduce gaps among policy, guidance, forms, and software. Reviewers can challenge a precise proposition instead of inferring behavior from code. Dependencies support regression planning and ownership.

Limits/adoption considerations

Traceability is only as complete as the maintained inventory. Policy rationales, discretionary judgments, and service-design considerations may not fit a proposition vocabulary and should remain first-class narrative artifacts. Organizations need setup review boards, semantic versioning, deprecation procedures, controlled source ingestion, and clear responsibility for each edge. Formal checks complement but do not replace policy conformity assessment, user research, accessibility testing, or software verification.
03Proposed-policy scenario and distributional-review sandbox

System/use case

A scenario sandbox allows analysts to compare how alternative policy formulations classify representative cases before a proposal is approved. Verified readback makes each scenario assertion reviewable, so discussion can separate the chosen rule structure from empirical forecasts and value judgments.

Operational setting

The sandbox supports option appraisal and implementation planning. Teams define baseline and proposed setups, synthetic cases, thresholds, and exceptions. A separate environment holds administrative data, microsimulation models, costing assumptions, and uncertainty ranges. Stakeholders can inspect formal readings without sensitive records.

Decision/claim boundary

The checked proposition states how a curated policy setup relates case features to a classification or process step. It does not establish causal impact, predict behavior, prove fiscal estimates, show distributional fairness, or determine that a scenario represents the population. Agda type correctness cannot validate parameter values or data. Policy owners authorize the rule interpretation; economists, statisticians, equality specialists, affected communities, and decision-makers remain responsible for their respective assessments.

Candidate checked statements

Illustrative candidates include:

  • “Under option B, every household meeting the revised threshold enters the qualifying cohort unless an approved exclusion applies.”
  • “If a representative case qualifies under the baseline but not the proposal, that case is classified as a transition loss.”
  • “Every scenario with an unresolved exception requires qualitative policy review.”

Example architecture

A registry versions cases, parameters, and provenance. FF Scribe checks propositions under baseline and candidate setups and retains readbacks. An evaluator applies approved propositions to synthetic or governed data. Microsimulation and costing consume classifications with explicit model versions and assumptions. A dashboard joins rule deltas to aggregate outcomes and impact evidence. Promotion requires policy authority and established decision processes.

Where verified readback fits

The analyst describes an expected rule or comparison in domain language. The model proposes a setup-limited Agda type, and the compiler checks its structural validity. If the partial readback stage supports that structure, ff-readback renders the audited candidates; otherwise it fails visibly. The analyst confirms whether a successful reading captures the proposed statement, and the policy owner separately authorizes the option’s interpretation or use. This records what rule was posed to the scenario engine; it neither proves the proposition from empirical data nor endorses the proposal. Factual validity, parameter authority, representativeness, and policy legitimacy remain independent review questions.

Potential benefits

Teams can compare options against stable, inspectable rule statements and detect where a changed threshold or exception alters classification. The separation of formal rule, scenario data, and simulation assumptions improves reproducibility and helps prevent a generated explanation from obscuring a modeling choice. It can also focus stakeholder review on cases where formalization is unsupported or transition treatment is unclear.

Limits/adoption considerations

Scenario outputs can create false precision when behavioral responses, take-up, administrative capacity, or data coverage are uncertain. Representative cases must be governed and complemented by empirical and participatory analysis. Setups need explicit effective periods and parameter provenance. The interface should show uncertainty, unsupported cases, and differences between rule classification and modeled outcome, with no automatic policy ranking or deployment.
04Appeals, reconsideration, and decision-explanation quality service

System/use case

A quality service checks whether proposed decision explanations and reconsideration routes reflect an approved policy structure. It helps case reviewers ensure that an outcome references relevant criteria, identifies missing evidence appropriately, and exposes available review paths without allowing generative text to invent a rationale.

Operational setting

The service operates before notice issuance or during reconsideration. It receives proposition identifiers, evidence statuses, policy version, reason codes, and route status. Personal information and documents stay in the case system. Independent reviewers see the checked rule and readbacks alongside the complete record.

Decision/claim boundary

The tool may check a proposition that certain recorded premises entail a program-defined outcome or review step. It does not decide disputed facts, assess witness credibility, validate an explanation as legally sufficient, or determine an appeal. It also does not prove that all relevant reasons were included. Authorized caseworkers, supervisors, hearing officers, tribunals, or courts retain their established responsibilities.

Candidate checked statements

Future controlled vocabularies might support candidates such as:

  • “If the only unmet condition is supported by evidence under review, the case remains pending rather than finally adverse.”
  • “Every adverse decision explanation identifies the applicable criterion and the recorded case finding.”
  • “If a reviewer overturns the original classification, the case requires a revised notice and decision record.”

Example architecture

The case system supplies findings and evidence status; a registry supplies criteria and reasons. FF Scribe checks propositions during authoring and controlled review. An explanation assembler uses accepted readbacks plus approved facts and templates. Quality checks flag absent criteria or inconsistent routes. Event records preserve determinations, setup versions, and reviewer actions. Authorized approval and accessibility standards govern notices.

Where verified readback fits

A policy owner or appeal specialist expresses the intended relation among a finding, disposition, and review route. The model forms a candidate in the relevant setup, and Agda checks its type. Supported structure yields the deterministic audited readback family; unsupported translation fails visibly. The author confirms whether a successful reading captures the intended statement or provides feedback, while the authorized policy or appeals role separately approves its use. The wording can anchor an explanation template, but it does not confirm real-world facts, demonstrate that a burden has been met, or validate the final notice. Meaning confirmation and adjudicative authority remain separate.

Potential benefits

The service can improve consistency of reason structures, reduce explanations that cite the wrong policy version, and make reconsideration transitions more traceable. It supports quality sampling by showing which checked rule and case findings underlay a draft disposition. Clear separation between missing evidence, a failed criterion, and an exception route may also improve procedural fairness and reduce avoidable appeals.

Limits/adoption considerations

Good explanations require context, plain-language and accessibility expertise, and often individualized reasoning beyond a finite readback. The service should never generate unreviewed adverse notices or suppress inconvenient evidence. Programs need independent appeals safeguards, record-correction mechanisms, bias monitoring, language access, retention controls, and transparent accountability. Audited readbacks must be revalidated whenever policy vocabulary or reason-code mappings change.
MLTTDB4 patterns
This catalogue expands the eligibility, thresholds, public-systems, impact-simulation, and explanation themes in ~/nn-ff-web/content/domains/policy.md. The examples are jurisdiction-neutral and illustrative; they are not statements of current policy or administrative law. Accountable policy owners, operational specialists, and qualified legal reviewers must approve each formalization and use.
01Public-benefit eligibility operations assurance

Operational context

A public agency or delegated administrator operates a benefit with categorical, household, income, residency, contribution, and exception criteria. Caseworkers collect evidence and make findings in a case-management system, while a policy operations team maintains procedure manuals and decision reason codes. The assurance need is to identify structurally incomplete or internally inconsistent proposed decisions before issuance and to test whether an approved operational rule set faithfully covers the policy’s modeled paths. It is not a replacement for caseworker judgment, evidence assessment, or appeal rights.

Why MLTTDB fits

Policy specialists can encode evidence statuses, household roles, threshold bands, qualifying conditions, exceptions, and outcome categories as distinct types rather than loosely coupled fields. A case projection then becomes an ordered, reviewable proof-assistant term. Propositions can require that an approval cites a complete qualifying path, that an adverse result exposes the failed condition and available review route, and that Unknown or disputed inputs lead to referral rather than being treated as false. Separating source declarations from stored scenarios also supports regression when a threshold or exception changes.

Example architecture

case system -> worker-confirmed findings -> minimal case projection adapter
policy instrument -> accountable formalization -> model repository
projection -> MLTTDB -> Agda/Lean/Rocq check -> supervisor queue -> case workflow

The case platform retains personal data, evidence, correspondence, and final authority. A privacy-minimizing adapter maps reviewed findings to the formal vocabulary and writes source-language rows. CI or the store launches the verifier against a pinned model. A result translator presents failed proof obligations and model assumptions to a supervisor. Only the external case workflow records approval, produces notice content, triggers payment, and manages reconsideration or appeal.

Representative typed artifacts

Declarations might include policyVersions :T: PolicyVersion, householdScenarios :T: HouseholdScenario, and decisionProposals :T: DecisionProposal. Types distinguish Submitted, Verified, Disputed, and Unavailable evidence and use an explicit ThreeWay result such as Qualifies, DoesNotQualify, or NeedsReview. Threshold values carry unit, household basis, period, and effective interval. A proposition such as supportedDecision connects only confirmed modeled findings to a proposed reason path. In Agda, proposals may look up earlier policy-version rows by UUID; portable models should avoid assuming the same capability in Lean or Rocq.

Checks and evidence

Schema mode checks a revised vocabulary before migration. Data mode rejects ill-typed projections, out-of-period policy references, missing reason routes, and attempts to use unresolved evidence as confirmed. Synthetic boundary suites cover values just below, at, and above thresholds; household transitions; exceptions; and incomplete evidence. External evidence records retain the model commit, policy approval identifier, ordered row UUIDs, source-case revision, verifier output, supervisor disposition, and notice revision. Sampling reconciles projections to the source file and tests explanation accessibility.

Potential benefits

The operation can catch incomplete reason paths earlier, make policy assumptions visible to supervisors, and distinguish genuinely adverse results from cases needing more evidence. Typed threshold units reduce common translation errors. Regression suites reveal which representative households change outcome under an approved amendment, while stable UUIDs let policy and delivery teams discuss the same cases. The result is better assurance evidence, not a claim of mechanically correct entitlement.

Deployment boundary

MLTTDB does not authenticate applicants, establish residency or income, assess credibility, interpret the governing instrument, decide eligibility, issue notices, make payment, detect fraud, or decide appeals. It does not guarantee fairness or legal compliance. Production use requires authorized decision-makers, privacy and security controls, accessibility, bias and equality review, explanation and challenge routes, source reconciliation, monitoring, and fail-safe manual processing. Policy owners and qualified legal reviewers approve all rules and release decisions.
02Grant-program award-criteria validation

Operational context

A grant-making body runs competitive programs with gateway eligibility, eligible-cost rules, strategic priorities, scoring rubrics, portfolio constraints, conflicts procedures, and delegated approval limits. Program officers and independent assessors work in a grants platform. Before a call opens, the policy team needs assurance that application forms, rubric configurations, and decision reason codes align with the approved scheme; before an award panel, it needs a consistency check on proposed decision packets without automating merit judgment.

Why MLTTDB fits

Formal types can keep gateway criteria separate from scored merit, advisory indicators, and portfolio-level considerations. This prevents an implementation from accidentally treating a high score as curing failed eligibility or treating an optional priority as mandatory. Typed rows can capture assessor-confirmed rubric selections, declared conflicts, moderation status, and proposed recommendations. Proof obligations can require complete scoring dimensions, valid delegation, explicit treatment of applicable exclusions, and a permissible reason code for each recommendation state.

Example architecture

approved scheme -> policy-to-model review -> versioned proof model
grant platform configuration -> configuration exporter -> MLTTDB assurance database
assessor packets -> batch verification -> exception dashboard -> panel secretariat

The proof model is developed and approved before program configuration. An exporter renders the actual grant-platform configuration and selected de-identified assessor packets into typed source terms, rather than maintaining an unconnected duplicate. A batch service fetches the ordered tables and runs proof-assistant validation. The exception dashboard groups failures by criterion or model proposition. The secretariat resolves discrepancies in the authoritative grants system and records panel and delegated decisions there.

Representative typed artifacts

Candidate tables include programCalls :T: ProgramCall, rubricDefinitions :T: RubricDefinition, assessmentPackets :T: AssessmentPacket, and delegations :T: Delegation. A Criterion records whether it is gateway, scored, tie-break, or advisory, plus evidence requirement and effective call. AssessmentPacket distinguishes raw assessor judgments from moderated values and the panel recommendation. A GrantConfigurationManifest aggregate term, reconciled to the platform export, enumerates the questions, reason codes, rubric criteria, and delegations used for whole-configuration checks. Propositions can then check that weights belong to the approved rubric, all mandatory dimensions represented in the manifest have dispositions, conflicted assessors do not supply counted scores, and the proposed approving role has sufficient delegation. Cross-row lookup can be concise in Agda; other backends need generated or embedded associations.

Checks and evidence

Pre-opening checks compare every configured question and reason code with its formal criterion and reject orphaned or duplicated mappings. Pre-panel checks validate packet completeness, score ranges, declared weighting arithmetic, moderation state, and delegation. Scenario fixtures include consortia, conditional awards, partial eligible costs, conflicts, tied rankings, and insufficient budgets. Evidence combines approved scheme and rubric identifiers, platform-configuration export hash, model revision, ordered UUIDs, checker transcript, exception resolutions, and panel approval record. A separate audit samples source assessments and access logs.

Potential benefits

Configuration errors can be found before applicants encounter them. Panels receive cleaner packets and a transparent separation between mechanical gateway checks and human merit judgments. Program changes become regression-testable, and delegation or conflict rules are less likely to be applied inconsistently. The retained validation evidence can support internal assurance and lessons learned without displacing the formal award record.

Deployment boundary

MLTTDB does not assess proposal quality, verify applicant assertions, manage conflicts, rank a portfolio, optimize a budget, award funds, or establish lawful authority. It is not a substitute for panel deliberation, procurement or subsidy-control analysis, financial due diligence, equality assessment, or legal review. Identity, documents, scoring workflow, audit logs, notifications, payments, and appeals remain external. Accountable officials approve the model and every funding decision.
03Permit and licence decision-table preflight

Operational context

A regulator or local authority administers several permit and licence classes. Each class has scope conditions, mandatory documents, fitness or technical findings, consultation steps, statutory or policy timeframes, conditions, renewals, and referral routes. Legacy workflow configurations often reproduce the same rules differently across channels. The proposed preflight service checks the decision table and a proposed application disposition for coherence before a designated officer acts; it does not create an automatic right to grant or refuse.

Why MLTTDB fits

A proof-assistant model can express permit class, activity scope, applicant role, evidence state, mandatory consultation, officer delegation, possible conditions, and terminal disposition as typed alternatives. Tables can hold reviewed rule profiles and synthetic or actual case projections. Propositions can require every in-scope application to reach either a permitted decision state or an explicit referral, prohibit conditions that are unavailable for the selected class, and prevent an expired evidence item from satisfying a modeled currency requirement. Unknown facts remain explicit instead of becoming default negatives.

Example architecture

policy and authority sources -> multidisciplinary rule workshop -> proof model
online portal/case system -> reconciliation adapter -> MLTTDB typed projection
officer preflight -> proof-assistant result -> reasoned human decision -> register

Policy, legal, operational, and subject-matter specialists jointly approve the model. The portal and case system remain authoritative for applications, evidence, fees, consultations, and correspondence. A reconciliation adapter creates a minimal projection with source revision identifiers. Verification may be initiated from the officer workbench through store orchestration, but semantic errors come from Agda, Lean, or Rocq. A decision service blocks release only according to separately approved workflow policy and records the officer’s independent disposition in the authoritative register.

Representative typed artifacts

The source might declare licenceClasses :T: LicenceClass, decisionProfiles :T: DecisionProfile, applicationProjections :T: ApplicationProjection, and conditionSets :T: ConditionSet. EvidenceStatus distinguishes received, validated, disputed, waived-with-authority, and expired. DecisionProfile associates mandatory findings and consultation paths with one effective policy version. A PermitConfigurationManifest aggregate term, built from and reconciled to the portal configuration export, enumerates routes, classes, evidence and reason codes, delegations, and condition templates. Decision procedures may compute proofs or counterexample data, but presenting that data requires a project-owned evaluator and result encoder; store-owned row evaluation is currently Agda-only. An Agda implementation can refer to earlier class and condition rows via literal UUID lookups; Lean/Rocq preprocessors require ordinary generated associations.

Checks and evidence

Configuration assurance checks the reconciled manifest: every enumerated portal route maps to one modeled class, required evidence codes are reachable, reason codes correspond to allowed outcomes, delegations are current in the modeled snapshot, and condition templates match class and decision. Case preflight checks completeness and consistency of the confirmed projection. Boundary fixtures cover renewals, changes of control, multiple activities, consultation objections, waiver authority, expiry, and manual referral. Evidence records the model and configuration revisions, manifest reconciliation, ordered UUIDs, source-case revision, verifier output, officer resolution, and final register entry in an external audit service.

Potential benefits

The authority can reduce channel-specific rule drift, uncover unreachable or contradictory configuration before deployment, and present officers with focused missing-input or incompatible-condition findings. Explicit referral states make uncertainty safer. Synthetic scenario suites improve communication between policy designers and delivery teams, while stable formal artifacts make changes easier to review across permit classes.

Deployment boundary

MLTTDB does not validate documents, inspect premises, assess fitness, resolve objections, determine jurisdiction, grant or revoke a licence, publish a register, or enforce conditions. It provides neither legal authority nor a complete administrative record. The surrounding system needs identity checks, payments, evidence custody, consultation, officer delegation, procedural fairness, accessibility, reasons, review and appeal, security, and manual continuity. Qualified policy, legal, and technical reviewers approve both formal rules and operational deployment.
04Policy-change impact and regression laboratory

Operational context

A central policy team is considering amendments to thresholds, definitions, exception routes, or transition provisions for an existing program. Analysts need to compare the current and proposed operational formalizations across a governed scenario library, understand which paths change, and identify implementation gaps before public consultation or rollout. Conventional spreadsheets are useful for costing but often hide classification assumptions and cannot demonstrate that all modeled cases reach a defined state.

Why MLTTDB fits

MLTTDB can hold ordered, stable scenario terms while separate proof-model branches encode current and candidate policies. The proof assistant can check scenario well-formedness and properties of the classification functions, such as exhaustiveness over a deliberately finite modeled domain, mutual exclusion of outcome constructors, or explicit NeedsReview handling. Running the same UUID-addressed scenarios against both branches yields a precise semantic regression set. This complements, rather than replaces, economic models and qualitative policy analysis.

Example architecture

research and consultation -> policy hypotheses -> current/candidate model branches
governed scenarios + declared paths/witnesses -> MLTTDB -> dual verification runs
checked declarations -> project-owned comparator -> impact review portal and teams

A scenario governance group approves synthetic archetypes, boundary cases, and any privacy-protected samples. Model authors encode proposals with traceable links to policy design decisions. For portability, each branch-specific scenario declaration carries a declared PolicyPath and a witness under that branch’s decision relation. A runner validates those declarations; a project-owned comparator then groups changed, unchanged, newly indeterminate, and invalid declarations and links them to assumptions. It does not treat generic validation output as a computed classification API. Costing, distributional analysis, operational design, and consultation use those findings as one input and remain separate systems and disciplines.

Representative typed artifacts

Tables could include scenarioCohorts :T: ScenarioCohort, policyScenarios :T: PolicyScenario, and expectedTransitions :T: ExpectedTransition. A scenario records units, time basis, evidence status, and explicitly bounded characteristics, never a loose map of fields. Each ExpectedTransition names a model branch, declares an algebraic PolicyPath and modeled reasons, and carries a witness that the branch’s decision relation admits that path. Propositions check total handling of the selected finite domain, transition-rule applicability, and preservation requirements identified by policy owners. In Agda, earlier-table UUID lookups can share cohort definitions; for backend portability, scenarios can be generated as self-contained terms.

Checks and evidence

The laboratory checks each branch’s declared paths and witnesses independently before the project-owned comparator compares those checked declarations. Regression gates flag changed paths, modeled reasons, required evidence, transition handling, and new proof failures. Metamorphic cases vary one modeled characteristic at a time to expose unexpected discontinuities; threshold fixtures cover boundary and unit conversions. Review evidence includes both commits, the scenario snapshot and ordered UUIDs, checker logs, comparison algorithm version, approved expected-change list, and reviewer dispositions. Statistical representativeness and fiscal estimates are validated by their own methods.

Potential benefits

Policy teams gain a concrete map from proposed wording and formal assumptions to representative operational effects. Unexpected changes can be discussed before implementation, and intended changes become explicit regression expectations. Reusable scenario identities improve collaboration among policy, legal, digital, and operations specialists. Formal checks can reveal gaps or contradictions that sensitivity tables alone miss.

Deployment boundary

MLTTDB does not forecast behavior, estimate expenditure, establish causal impact, determine distributional fairness, run consultation, interpret source law, or approve policy. Scenario coverage does not guarantee population coverage, and a proof is only about the formal model and supplied terms. Production decisions require empirical analysis, equality and rights assessment, legal review, stakeholder participation, privacy governance, implementation testing, and accountable authorization. The laboratory must clearly label assumptions and never present illustrative outputs as official entitlements.
State Machine Studio3 demos
SMEmergency relief delivery

This example represents delivery of time-critical public assistance after a disaster or emergency while preserving eligibility, authorization, delivery, and reconciliation controls. It recognizes the central operational tension: a program must act quickly enough to meet immediate safety and subsistence needs, yet still prevent duplicate, diverted, or unsupported payments and retain a reviewable explanation of who received what assistance.

The workflow starts by capturing the immediate need and contact details and assigning a traceable relief case. Urgency triage evaluates safety and the time available to act, then selects standard or expedited handling under published criteria. Standard cases proceed through event, location, and household verification. Missing evidence can return the request to intake for completion. In an expedited case, emergency evidence exceptions are documented and authorization may occur before the normal evidentiary package is complete; expedited handling changes the sequence, not the obligation to account for the decision.

Authorization calculates the permitted assistance package and approves the delivery channel and its controls. Delivery dispatches funds, goods, or services and confirms recipient access. A failed, duplicate, or diverted delivery opens an exception and protects remaining value while staff investigate. A corrected exception can resume delivery, while a conflict in entitlement, amount, or channel returns for reauthorization. Confirmed delivery advances to reconciliation, where the case team compares authorization with delivery records and publishes a reviewable outcome. A later reconciliation gap reopens the exception rather than being written off as administratively complete.

These controls matter because emergency conditions weaken ordinary evidence sources, displace households, create urgency, and attract fraud attempts at the same time. A traceable case identifier and explicit expedited criteria support equitable triage. Bounded authorization and delivery controls limit loss without delaying every case. Reconciliation allows the program to act on provisional evidence while preserving accountability to affected people, program managers, finance teams, and public auditors.

Layer 1 — Emergency relief lifecycle

This layer gives incident leadership the end-to-end status of relief cases: received, triaged, verified, authorized, delivering, reconciled, or in exception. It makes the expedited route and recovery loops visible across the program. It deliberately excludes specific identity checks, payment instructions, and delivery confirmations so leaders can assess reach, bottlenecks, and control exposure during the event.

Layer 2 — Relief case operations

This is the coordination view for intake teams, eligibility staff, authorizers, delivery partners, and reconciliation staff. It covers triage categories, verification standards, emergency exceptions, benefit calculation, channel approval, dispatch, failed-delivery handling, reauthorization, and closeout reconciliation. It includes ownership and handoffs but excludes each system field, document query, or payment API call.

Layer 3 — Relief checks and actions

This layer contains case-level execution: capture needs, check event and location, document a waived or deferred item, calculate the permitted package, issue funds or goods, confirm access, detect duplicates, protect unspent value, and reconcile authorization to delivery. It provides a reproducible decision and disbursement trail while leaving event-wide policy choices and lifecycle posture to the higher layers.
Open interactive model
SMHousing assistance determination

This example represents a public housing-support determination from application through evidence review, eligibility decision, payment authorization, renewal, material-change review, denial, and appeal. It treats eligibility as a reasoned case decision rather than a single income comparison: household composition, residence, housing cost, need thresholds, evidence rules, exceptions, and the applicable policy period all contribute to the outcome.

The workflow starts by registering the household application and issuing clear evidence and consent requirements. Case staff verify household, residence, and cost records and resolve omissions or inconsistent declarations. Incomplete evidence returns to intake so the applicant can respond instead of producing an unexplained adverse decision. Once the record is complete, the eligibility decision applies income and need thresholds, records any authorized exception, and produces an explanation tied to the relied-upon criteria.

An eligible household moves to active assistance, where the payment schedule is authorized and renewal and change-reporting obligations are monitored. A household that does not meet the criteria receives reasons and an open reconsideration window. A timely appeal assembles the original decision record and routes new evidence to independent review; review can uphold the denial or reverse it and activate assistance. Active cases are not assumed to remain static. A reported material change pauses payments only under the applicable rule and triggers review. Cleared changes restore assistance, disqualifying changes produce a reasoned denial, and scheduled renewals return the case to evidence review.

These controls matter because small factual or policy differences can affect access to essential housing support. Clear evidence requests reduce avoidable attrition, a recorded rule path supports consistent decisions across caseworkers, and independent appeal prevents the original conclusion from becoming self-validating. Renewal and change controls protect public funds while ensuring that suspension or denial follows an authorized process and remains explainable to the household, supervisors, auditors, and review bodies.

Layer 1 — Housing assistance lifecycle

This layer is the program and case-status view: received, under evidence review, decided, active, denied, appealed, or suspended. It shows the full route to assistance and the safeguards around adverse or changed decisions. It intentionally excludes document-level verification, calculation fields, and payment-system commands so policy owners can see throughput, fairness checkpoints, and unresolved case posture.

Layer 2 — Eligibility case operations

This is the operational view for caseworkers, supervisors, appeal officers, and payment administrators. It covers evidence requests, verification, threshold application, decision notices, reconsideration windows, independent review, renewal, material-change handling, and restoration or denial. It includes handoffs and decision authority but excludes individual database updates and field-by-field evidence checks.

Layer 3 — Decision checks and actions

This layer contains the concrete case actions: register the household, verify residence and housing cost, resolve declarations, calculate relevant income and need, record exceptions, issue reasons, assemble the appeal record, authorize a schedule, and pause or restore payment. It supports an auditable decision trace while leaving policy-wide performance and lifecycle status to the higher layers.
Open interactive model
SMPublic grant administration

This example represents a competitive public-grant program from publication of the funding opportunity through eligibility screening, merit assessment, award, performance monitoring, remediation, and closeout. It connects the approved policy objectives and assessment criteria to award decisions, milestone payments, outcome evidence, expenditure review, and the retained public record.

The workflow begins when the authority publishes objectives, thresholds, exclusions, submission rules, and a controlled clarification record. After the submission window closes, applications are screened for timeliness and applicant eligibility. Curable defects return through the published clarification or correction route; non-curable conditions are recorded consistently. Eligible proposals proceed to assessment against the approved criteria, with conflicts of interest and moderation evidence captured. An inconsistency can reopen screening rather than allowing an unreliable score to advance.

An approved proposal becomes an active award with executed conditions and funding released only against authorized milestones. Monitoring reviews outcome and expenditure evidence and applies defined variance and change-control thresholds. Completed milestones and satisfactory final records permit closeout. Non-performance, an award-condition breach, or a closeout gap enters remediation. The response may be a corrective plan followed by renewed monitoring, reissued award terms, suspension, or recovery action. Even a nominally closed grant can reopen if final financial or outcome evidence does not support closure.

These controls matter because public funding decisions must be fair, consistent, and demonstrably connected to published purposes. Controlled clarifications avoid giving one applicant an informational advantage. Eligibility screening and conflict management protect the integrity of competition, while moderated scoring makes judgment reviewable without pretending it is mechanical. Milestone controls, documented variations, and remediation protect public money and program outcomes. A retained decision and audit trail supports applicants, oversight bodies, auditors, and the public in understanding both selection and post-award stewardship.

Layer 1 — Public grant lifecycle

This layer is the portfolio and governance view: opportunity published, applications screened, proposals assessed, award active, performance monitored, grant closed, or remediation underway. It shows the main accountability gates from appropriation intent to closeout. It intentionally excludes individual score entries, invoice checks, and payment operations so program leaders can see competition status, award health, and unresolved exposure.

Layer 2 — Grant administration operations

This is the working view for program officers, assessment panels, grants finance, contract managers, and assurance staff. It covers publication and clarifications, eligibility screening, scoring and moderation, conflict handling, award conditions, milestone releases, variation control, monitoring, remediation, recovery, and closeout. It includes the operational decision points but excludes atomic document and system actions.

Layer 3 — Grant checks and actions

This layer contains the evidence-bearing tasks: test submission and applicant eligibility, record defects, score criteria, declare conflicts, retain moderation reasons, execute conditions, validate milestone and expenditure evidence, apply variance thresholds, issue corrective actions, and reconcile final records. It is detailed enough to audit a decision or payment while leaving program-wide policy and lifecycle posture to the higher layers.
Open interactive model
Explore patternsReview product applications

Cabinet index

Explore Formal Foundry

Book a meeting Explore libraries

Trusted systems. Mathematical proofs.

Search the archive

Find a page

Type to search the published content.