Clinical
Challenges
- Eligibility rules depend on changing observations, thresholds, and histories.
- Contraindications can be distributed across protocols and reference material.
- Safety exceptions require clear escalation and accountable review paths.
- Clinical logic must remain inspectable as guidance and evidence evolve.
Problems We Solve
- Criteria Representation Structure eligibility conditions and relevant observations.
- Contraindication Checking Identify conflicts between proposed actions and safety rules.
- Pathway Simulation Explore decision paths across representative scenarios.
- Safety Validation Check escalation triggers and required protective actions.
- Review Support Prepare traceable summaries for qualified human review.
Domain portfolio
Application patterns
Compare two formal-assurance approaches, then explore the domain workflows as interactive state machines.
01 Emergency-department deterioration and escalation support Explore pattern
System/use case
Operational setting
Decision/claim boundary
Candidate checked statements
Illustrative controlled-English propositions for a future setup include:
- “Every patient state with a confirmed high-acuity trigger requires clinician reassessment.”
- “If a required reassessment is overdue, the pathway enters an escalation state.”
- “A discharge-ready state is unavailable while an unresolved critical observation remains active.”
- “Every escalation state identifies a responsible clinical review role.”
These are candidate formalization schemas, not implemented clinical rules or recommendations.
Example architecture
Where verified readback fits
ff-readback produces a deterministic audited family with premise order and semantic-rule provenance intact; unsupported structure fails visibly. The informatician confirms whether a reading captures the authored statement, while a qualified clinician separately approves or rejects its clinical content. Neither action authorizes deployment or application to a patient.Potential benefits
Limits/adoption considerations
02 Medication contraindication and order-review support Explore pattern
System/use case
Operational setting
Decision/claim boundary
Candidate checked statements
Potential controlled-English propositions include:
- “Every proposed medication order with an active contraindication requires qualified clinical review.”
- “A contraindication cannot be marked resolved while its required evidence remains pending.”
- “If duplicate-therapy review is required, order verification depends on completion of that review.”
- “Every overridden safety flag records an accountable reviewer role.”
These statements are illustrative and deliberately avoid asserting any particular drug rule or threshold.
Example architecture
Where verified readback fits
Potential benefits
Limits/adoption considerations
03 Clinical-trial eligibility prescreening Explore pattern
System/use case
Operational setting
Decision/claim boundary
Candidate checked statements
Illustrative propositions include:
- “Every prescreening candidate satisfies each represented inclusion criterion.”
- “Any unresolved exclusion criterion routes the record to manual review.”
- “Missing required evidence cannot be treated as evidence that the criterion is satisfied.”
- “A prescreening match is distinct from a confirmed eligibility decision.”
They are proposed controlled-language targets, not a translation of any current protocol.
Example architecture
Where verified readback fits
Potential benefits
Limits/adoption considerations
04 Oncology treatment-pathway review support Explore pattern
System/use case
Operational setting
Decision/claim boundary
Candidate checked statements
Possible controlled-English propositions include:
- “Every pathway branch with unresolved prerequisite evidence remains pending clinical review.”
- “An active modeled contraindication prevents the branch from becoming pathway-eligible.”
- “Every discordant diagnostic-evidence state routes to multidisciplinary review.”
- “A pathway-eligible state is decision support and is not a treatment authorization.”
These are illustrative proposition forms rather than clinical recommendations.
Example architecture
Where verified readback fits
Potential benefits
Limits/adoption considerations
Applicability frame
MLTTDB can plausibly validate finite, versioned clinical configuration packs or typed review packets. Proof-assistant source owns the clinical abstractions, row types, table declarations, invariants, and proofs. The SQLite term store owns ordered source-language records, UUIDs, metadata, and stored table definitions; it neither interprets clinical meaning nor establishes that a source observation is correct. Semantic checking is performed by Agda, Lean, or Rocq, even when the store orchestrates the checker subprocess. Agda currently supports finite lookup of stored rows by literal UUID. Lean and Rocq preprocessors currently generate and check definitions but do not support that lookup form.
Current data mode checks fetched rows as separate definitions; it does not expose a table to application proofs as an enumerable, first-class collection. Whenever an example below claims whole-snapshot coverage, uniqueness, or graph acyclicity, the architecture therefore assumes either a finite domain declared in proof source or an external snapshot compiler that emits a reconciled aggregate manifest/certificate term. The proof assistant checks that aggregate term, while external reconciliation establishes that it represents the table export supplied for review.
EHR, trial-management, pharmacy, laboratory, and blood-bank ingestion; terminology and patient-identity reconciliation; consent; access control; workflow orchestration; runtime alerts or hard stops; audit retention; and clinical formalization review are external production responsibilities. A successful check means the encoded artifacts satisfy the encoded properties under declared assumptions. It cannot establish diagnosis, data timeliness, patient identity, complete documentation, or an appropriate clinical action.
01 Clinical-trial eligibility and contraindication review pack Explore pattern
Operational context
Why MLTTDB fits
Example architecture
protocol/amendment repository ---> criteria authoring + dual clinical review
|
EHR/CTMS extracts -> identity/terminology reconciliation -> typed review pack
|
v
MLTTDB term store
|
proof-owned eligibility model ----------------------+--> proof-assistant check
|
review report -> investigator/CTMS
A validated authoring process translates the protocol into reviewed formal criteria. A separate site integration resolves patient, visit, laboratory, and terminology identifiers and presents provenance to coordinators. The term store holds source-language rows for a specific protocol and review packet. The checker returns validation status and native diagnostics. A project-owned adapter associates diagnostics with row UUIDs, maps them into reviewer-facing findings, and retains any explicitly generated proof artifacts. The CTMS records the accountable investigator’s disposition through its own workflow.
Representative typed artifacts
ProtocolVersion,Cohort, andCriterion, with explicit applicability and amendment provenance.EvidenceItem, carrying category, observation time relation, source reference, verification status, and an explicit unknown/indeterminate case.CriterionAssessment, linking a criterion to reviewed evidence and a reasoned state such as satisfied, not satisfied, or unresolved.ContraindicationGroupandEscalationRequirementfor investigator review.- An
EligibilityReviewManifestaggregate term, built by the reviewed adapter and reconciled to protocol, criterion, evidence, and assessment row UUIDs. - Proof obligations for complete criterion coverage, protocol-version alignment, contradiction detection, and no positive modeled conclusion from unresolved required evidence.
Checks and evidence
Potential benefits
Deployment boundary
02 Oncology regimen-library release guardrails Explore pattern
Operational context
Why MLTTDB fits
Example architecture
clinical governance source + formulary + vendor build export
|
terminology mapping and pharmacist reconciliation
v
MLTTDB regimen candidate baseline
|
proof-owned regimen model -> proof-assistant check
|
release dossier + exact configuration digest
v
CPOE/pharmacy build validation, simulation, approval, deployment
External tooling maps vendor concepts and medication identifiers to the formally reviewed catalogue. MLTTDB stores the ordered proof-language records and can expose verification through CI or an administrative service. A release controller binds the result to the vendor import package. Pharmacists and clinicians then inspect rendered templates and execute simulation and user acceptance tests before activating the configuration.
Representative typed artifacts
RegimenTemplate,TreatmentPhase, andRegimenComponent, each with stable identity and source provenance.AdministrationConstraint, describing abstract route, sequence, or co-administration relationships without inventing clinical content.ObservationRequirement,AdjustmentBranch, andHoldEscalation, including an explicit “requires clinician resolution” outcome.SupportiveCareDependencyandAlternativeBranch, with applicability conditions reviewed by domain experts.- A
RegimenReleaseManifestaggregate term, reconciled to the vendor-package export and row UUIDs, enumerating the phases, components, branches, observations, and dependencies in the candidate release. - Proofs for reference closure, phase/component consistency, dependency presence, branch exclusivity, and complete modeled exception disposition.
Checks and evidence
Potential benefits
Deployment boundary
03 Transfusion episode safety-gate configuration Explore pattern
Operational context
Why MLTTDB fits
Example architecture
transfusion policy + LIS/EHR/device workflow dictionaries
|
laboratory/clinical informatics reconciliation
v
MLTTDB gate-configuration baseline
|
proof-owned episode model -> checker service
|
verified rule map + release evidence
v
LIS/EHR/device integration tests -> transfusion governance approval
An external mapping layer aligns system-specific status and reason codes with a clinically governed formal vocabulary. The term store persists candidate rules as proof-language records. The checker validates the modeled transition system; integration-test harnesses then exercise the actual LIS, EHR, label, scanner, and device interfaces. A release record correlates all evidence with the deployed configuration version.
Representative typed artifacts
EpisodeStage,EvidenceClass, andGateRequirement, with explicit provenance and validity-state semantics.ComponentStatusandIdentityEvidence, modeled as reviewed categorical states rather than values inferred by MLTTDB.PermittedTransition, with source stage, required evidence set, accountable role, destination, and failure destination.ExceptionPathfor urgent, mismatch, unavailable-data, or reaction workflow categories defined by the organization.- An
EpisodeGateManifestaggregate term, reconciled to the policy export and row UUIDs, materializing the states, evidence classes, transitions, and exception paths used for graph-wide checks. - Proofs for prerequisite completeness, stop-state absorption, exception escalation, and absence of an unreviewed path to the modeled ready state.
Checks and evidence
Potential benefits
Deployment boundary
04 Discharge medication-reconciliation review packet Explore pattern
Operational context
Why MLTTDB fits
Example architecture
EHR/pharmacy/external lists -> patient + terminology reconciliation
|
clinician review workspace
|
typed candidate snapshot
v
MLTTDB term store
|
proof-owned reconciliation invariants +--> proof-assistant verification
|
consistency report -> clinician sign-off/EHR
Identity, terminology, duplicate detection, and source provenance are resolved by clinical integration services and displayed to the reviewer. Only the reviewed categorical statements needed by the formal model are serialized to MLTTDB, preferably with data minimization or pseudonymous references. The verification result returns to the workspace as an internal-consistency aid. The EHR owns the legal record, prescribing actions, attestation, and downstream communication.
Representative typed artifacts
SourceMedicationStatement, with source system, provenance reference, confidence/review state, and encounter scope.ReconciledMedication, grouping reviewed source statements under a canonical identity assigned by external terminology services.Disposition, representing continue, change, stop, replace, defer, or unresolved categories as locally governed abstractions.Discrepancy,FollowUpObligation, andCommunicationTargetrecords.- A
MedicationReconciliationManifestaggregate term, reconciled to the minimal EHR projection and row UUIDs, enumerating source statements, grouped medications, dispositions, and communication obligations. - Proof obligations for source-statement coverage, disposition exclusivity, unresolved-item escalation, and complete modeled communication obligations before readiness.
Checks and evidence
Potential benefits
Deployment boundary
These read-only, pan-and-zoom models expose three abstraction levels for each workflow. They are explanatory examples, not live operational or decision systems.
Patient Deterioration Response
About this workflow
This example represents recognition and response when a patient’s observations begin to depart from their expected course. It joins trend monitoring, validation of warning signals, qualified triage, time-critical intervention, reassessment, and care transition. The model accommodates a local early-warning policy or specialty pathway without assuming that one threshold or score is appropriate for every patient.
The pathway starts with patient-specific baseline observations, scheduled trend and symptom assessments, active risk modifiers, and monitoring limits. When a warning appears, staff validate the measurement and timestamp, compare the trend with the applicable threshold, and notify the accountable care role. Clinical triage combines symptoms, trend severity, relevant history, and the governing safety pathway to determine urgency and whether local review or rapid-response escalation is required. A protective intervention assigns qualified actions, monitoring, and communication responsibilities while recording the timing and observed response. Protocol-defined reassessment repeats the necessary observations and compares them with stabilization criteria. A stabilized patient returns to baseline monitoring; unresolved deterioration moves to a care transition with the current condition, risks, and intervention timeline handed off and acknowledged.
The loops distinguish false alarms from unresolved risk without normalizing either. A confirmed measurement artifact can return to routine monitoring, but only after validation. Triage may restore monitoring when qualified assessment finds no continuing concern, or initiate an urgent care transition without waiting for a local intervention cycle. Reassessment can repeat or adjust the intervention when response is inadequate. Failure to meet stabilization criteria escalates care rather than resetting the warning. These controls matter to bedside nurses, treating clinicians, and rapid-response teams because delayed escalation often results from fragmented observations, unclear ownership, or failure to confirm response after an intervention. Explicit handoff acknowledgement reduces the chance that unresolved deterioration disappears between teams or care settings.
Layer 1 — Deterioration pathway
Layer 2 — Escalation and reassessment procedures
Layer 3 — Observation-level actions
High-Risk Medication Administration
About this workflow
This example represents the closed-loop administration of a high-risk medication, from drafting the order through verification, patient-specific preparation, bedside checks, post-dose monitoring, and completion or safety escalation. It emphasizes that safe administration depends on current clinical observations and independent controls, not solely on the presence of a signed order.
The normal pathway begins with the medication, indication, route, schedule, and protocol-specific monitoring requirements, linked to current weight, renal function, hepatic function, and other dose-relevant observations. Clinical verification checks allergies and prior reactions, drug interactions, duplicate therapy, contraindications, and dose calculation. Pharmacy or the authorized preparer selects the verified product and concentration, prepares and labels the patient-specific dose, and completes the required independent check. At the bedside, the care team matches patient, medication, dose, route, and time; confirms baseline observations; and verifies access to rescue resources and escalation contacts. After administration, protocol-defined response and safety signals, vital signs, and relevant laboratory results are trended and documented before therapy is completed.
The return and escalation paths keep new information from being bypassed. An unsafe or incomplete order returns to the prescriber for revision. A preparation mismatch found at the bedside goes back for correction rather than being informally reconciled. A newly identified contraindication before dosing, or an adverse signal afterward, enters safety escalation: further dosing is held, the patient is assessed, the protective response is initiated, and qualified review is required. The reviewed outcome may produce a new order and controlled resumption or terminate therapy. These controls matter to prescribers, pharmacists, nurses, and safety teams because renal function, weight, concurrent therapies, and patient condition can change between ordering and administration, while independent verification and prompt reaction management reduce preventable harm.
Layer 1 — Medication pathway
Layer 2 — Safety verification procedures
Layer 3 — Bedside actions
Clinical-Trial Screening and Enrollment
About this workflow
This example represents a candidate’s pathway from referral to a documented trial-screening disposition. It brings informed consent, protocol-defined eligibility, time-sensitive observations, contraindications, washout conditions, and qualified exception review into one inspectable workflow. It is not a substitute for the protocol or investigator judgment; it shows how the evidence and decisions required by those authorities should progress.
The expected pathway begins by confirming the candidate, requested cohort, and enrollment window. The current approved consent materials are presented before study-specific screening, and the team documents questions, decision-making capacity, voluntary agreement, and the consent version used. Screening then collects protocol-required history, examinations, laboratory results, and imaging, checking freshness windows as well as washout and concurrent-treatment conditions. Eligibility review evaluates each inclusion criterion, checks exclusions and distributed contraindications, and produces a criterion-by-criterion summary. A qualified candidate receives a cohort and enrollment identifier, with protocol activities and safety monitoring scheduled. The final disposition and its supporting record are retained when screening closes.
The exception paths reflect real screening work. Withdrawal after consent closes the candidate without proceeding. A stale laboratory result or observation returns for refresh rather than being treated as current. An ambiguous finding, missing evidence, or out-of-window assessment goes to protocol-authorized qualified review. The reviewer records the issue, authority, disposition, and rationale, then either returns the record for reassessment or closes an unresolved screening. A clearly ineligible candidate also closes without enrollment. These controls matter to investigators, coordinators, and monitors because enrollment pressure must not turn uncertainty into assumed eligibility, and because consent version, observation timing, contraindication review, and documented investigator decisions are central to participant safety and trial integrity.