Skip to main content

FM-2 formal verification of CDR-to-FHIR mappings — Allen algebra, Z3 SMT proofs, SILD silent information loss detection.

Project description

CAIRN

Clinical interoperability reference architecture. Built on FM-2.

Version Licence: EUPL-1.2 Python 3.11+ DOI PyPI Tests NOT a Medical Device


⚠️ CAIRN is NOT a medical device as defined by EU MDR 2017/745, EU IVDR 2017/746, or MPDG. It is a mathematical framework for research and interoperability validation only. It does not process real patient data in production contexts.


What is CAIRN?

CAIRN is an open-source reference architecture for formal verification of clinical interoperability mappings. It implements FM-2 — a mathematical framework modelling clinical data through:

  • a type system as a directed acyclic graph (DAG)
  • Allen temporal algebra (13 interval relations)
  • a universal event model as a 6-tuple: (id, type, temporal, value_set, context, provenance)
  • Z3 SMT proofs for value-space containment and structural preservation
  • SILD (Silent Information Loss Detector) for CDR-to-FHIR mapping verification

CAIRN answers a practical question:

What is silently lost when clinical data moves from one system to another — and how can we prove it formally, before production?


Was ist CAIRN?

CAIRN ist eine offene Referenzarchitektur für die formale Verifikation klinischer Interoperabilitäts-Mappings. Sie implementiert FM-2 — ein mathematisches Modell klinischer Daten auf Basis von:

  • einem Typsystem als gerichtetem azyklischen Graphen (DAG)
  • Allen-Temporalalgebra (13 Intervallrelationen)
  • einem universellen Ereignismodell als 6-Tupel: (id, type, temporal, value_set, context, provenance)
  • Z3 SMT-Beweisen für Werteraum-Containment und Strukturerhalt
  • SILD (Silent Information Loss Detector) zur CDR-zu-FHIR-Verifikation

Was geht beim Datentransfer zwischen klinischen Systemen still verloren — und wie lässt sich das formal nachweisen, bevor es in Produktion geht?


Real-World Loss Patterns Detected by CAIRN

Loss Class Clinical Example FM-2 Formalism SILD Class
Temporal precision Anaesthesia 08:12–11:47 → 00:00–23:59 Allen: DURING REGRESSION
Negation absence "No known allergy" → empty FHIR Bundle Cardinality n→0 SILENT_LOSS
Terminology drift SNOMED laterality → ICD-10-GM (lost) Value-space ⊊ DRIFT
HL7 field mapping Cholesterol ref. range + "H" flag dropped Z3: not surjective PERSISTENT
Cardinality collapse 4 CDR diagnoses → 2 FHIR diagnoses φ_B: CDR ≠ FHIR REGRESSION

Quickstart

pip install cairn-clinical
from cairn.adapters import FHIRAdapter
from cairn.verification import SILDAnalyzer

# Load CDR source and FHIR target
adapter     = FHIRAdapter()
cdr_events  = adapter.load_bundle_file("source_cdr.json")
fhir_events = adapter.load_bundle_file("mapped_fhir.json")

# Detect silent information loss
report = SILDAnalyzer().compare(cdr_events, fhir_events)
report.print_summary()
════════════════════════════════════════════════════════════════
 CAIRN / SILD Report  —  2026-05-25 09:00
════════════════════════════════════════════════════════════════
 Source : CDR  (5 events)
 Target : FHIR-R4  (3 events)
────────────────────────────────────────────────────────────────
 [SILENT_LOSS|CRITICAL] AllergyStatement/716186003: Negated event absent in FHIR
 [REGRESSION|HIGH]      Anaesthesia/72641008: Temporal precision lost (215min → 1439min)
 [DRIFT|HIGH]           TerminologyDrift/416098002: SNOMED laterality → ICD-10-GM (lost)
 [REGRESSION|MEDIUM]    LabResult/2093-3: Value-space not preserved: missing referenceRange
────────────────────────────────────────────────────────────────
 Total: 4 findings | 2 regressions | 1 silent losses | 1 critical
════════════════════════════════════════════════════════════════
# CLI
cairn verify   --source cdr.json  --target fhir.json  --output report.json
cairn drift    --source cdr.json  --target fhir.json
cairn variance --files a.csv:HausA:Orbis  --files b.csv:HausB:iMedOne
cairn version

Version comparison (IMPROVEMENT detection)

# Compare two mapping versions — detect improvements and regressions
report_v1 = SILDAnalyzer().compare(cdr_events, fhir_v1_events, mapping_version="1.0")
report_v2 = SILDAnalyzer().compare(cdr_events, fhir_v2_events, mapping_version="2.0",
                                    reference_report=report_v1)
# IMPROVEMENT findings mark event codes resolved since v1
report_v2.print_summary()

Modules

Module Contents
cairn.core Type DAG · Allen algebra (13 relations) · 6-tuple event model · Homomorphism checker
cairn.verification Z3 SMT proofs · Value-space containment · SILD engine (all 6 classifications)
cairn.adapters FHIR R4 · HL7 v2 (ORU/ADT/RXA) · CSV/DataFrame
cairn.analysis Cohort queries φA–φD · Terminology drift (8 system pairs) · Multi-site KIS variance
cairn.api FastAPI REST (POST /verify · POST /drift · GET /health)
cairn.cli Click CLI (verify · drift · variance · version)

Architecture

cairn/
├── core/
│   ├── allen.py          # Allen temporal algebra — 13 interval relations
│   ├── event.py          # Universal event model — 6-tuple (FMEvent)
│   ├── homomorphism.py   # Structure-preservation checker
│   └── type_dag.py       # Type system as directed acyclic graph
│
├── verification/
│   ├── sild.py           # Silent Information Loss Detector (SILD)
│   └── z3_proofs.py      # Z3 SMT formal proofs
│
├── adapters/
│   ├── csv_df.py         # CSV / pandas DataFrame
│   ├── fhir_r4.py        # FHIR R4 (Observation, Condition, Procedure, ...)
│   └── hl7v2.py          # HL7 v2 (ORU^R01, ADT^A01, RXA)
│
├── analysis/
│   ├── cohort.py         # FM-2 cohort queries φA–φD
│   ├── terminology.py    # Terminology drift checker (8 system-pair mappings)
│   └── variance.py       # Multi-site completeness variance (KIS comparison)
│
├── api/
│   └── app.py            # FastAPI REST API
│
└── cli/
    └── commands.py       # Click command-line interface

tests/
├── unit/                 # FM-2 core + CLI + API (32 tests)
├── integration/          # SILD — all 5 real-world loss patterns + drift (8 tests)
└── property/             # Hypothesis property tests — FM-2 invariants P1–P6

Dependencies

CAIRN is built exclusively on publicly available PyPI libraries. All dependencies with their licences are documented in NOTICE.

# Core
networkx       >= 3.2    # Type DAG, homomorphism       BSD-3-Clause
z3-solver      >= 4.12   # SMT formal verification       MIT
pydantic       >= 2.5    # Schema validation             MIT
pandas         >= 2.1    # DataFrame adapter             BSD-3-Clause

# Healthcare standards
fhir.resources >= 7.1    # FHIR R4                      BSD-3-Clause
hl7            >= 0.4    # HL7 v2 parsing               BSD-3-Clause

# API & CLI
fastapi        >= 0.110  # REST API                      MIT
httpx          >= 0.27   # API test client               BSD-3-Clause
click          >= 8.1    # CLI                           BSD-3-Clause

Tests

pip install -e ".[dev]"
pytest tests/ -v
50 passed in 3.16s

tests/unit/        32 tests  (Type DAG · Allen algebra · event model · CLI · API)
tests/integration/  8 tests  (5 SILD loss patterns + terminology drift)
tests/property/     6 tests  (Hypothesis: FM-2 invariants P1–P6)

Licence

CAIRN is licensed under the European Union Public Licence v. 1.2 (EUPL-1.2).

  • Free to use, modify, and distribute
  • Modifications must be contributed back under the same licence
  • Copyleft covers network use (SaaS)
  • Legally valid in all EU member states in their official languages

See LICENCE for the full text.


Not a Medical Device

CAIRN is a mathematical research tool. It is not a medical device under:

  • EU MDR 2017/745 (Medical Device Regulation)
  • EU IVDR 2017/746 (In Vitro Diagnostic Regulation)
  • MPDG — Medizinprodukterecht-Durchführungsgesetz (Deutschland)

See NOTICE for the complete disclaimer.


Contributing

Contributions are welcome under EUPL-1.2. By contributing, you agree your changes will be returned to the reference system.


Citation

@software{cairn2026,
  title   = {CAIRN — Clinical interoperability reference architecture},
  author  = {Matten, Friedhelm},
  year    = {2026},
  doi     = {10.5281/zenodo.20375036},
  url     = {https://github.com/fmatten/CAIRN},
  licence = {EUPL-1.2},
  version = {1.0.1}
}

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

cairn_clinical-1.0.2.tar.gz (113.1 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

cairn_clinical-1.0.2-py3-none-any.whl (48.7 kB view details)

Uploaded Python 3

File details

Details for the file cairn_clinical-1.0.2.tar.gz.

File metadata

  • Download URL: cairn_clinical-1.0.2.tar.gz
  • Upload date:
  • Size: 113.1 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.13.5

File hashes

Hashes for cairn_clinical-1.0.2.tar.gz
Algorithm Hash digest
SHA256 bce1e38b04f42520e381f7bd5cfa0db8c04b9d7d1a6cfeea12f899dabdfd7703
MD5 6d9a567ed7fea3e682e25f6c6f8c3755
BLAKE2b-256 d5ab0b657b1c85560042a7eddf153e04832294242d07b3041f1c5de468b72176

See more details on using hashes here.

File details

Details for the file cairn_clinical-1.0.2-py3-none-any.whl.

File metadata

  • Download URL: cairn_clinical-1.0.2-py3-none-any.whl
  • Upload date:
  • Size: 48.7 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/6.1.0 CPython/3.13.5

File hashes

Hashes for cairn_clinical-1.0.2-py3-none-any.whl
Algorithm Hash digest
SHA256 333a88329f337a2cbf61a9692818c1960d22ece298ee67444837b71de0400ec4
MD5 b9ae0de411b145ccd93f5d66c337e34e
BLAKE2b-256 c238a4ecff7c3c49eba32ac4de09b69d5f23706843b128e43bc571df316edb14

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page