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: AGPL-3.0 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 GNU Affero General Public License v3 (AGPL-3.0-only OR Commercial).

  • 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.


Related Projects

Project Description DOI / Link
FM-1 Grundlagen zur wissenschaftlichen Auswertung von klinischen Informationen 10.5281/zenodo.19205557
FM-4 / SILD Signal-Loss Inspection at Data-boundaries — Theoriepaper zu CAIRN 10.5281/zenodo.20375435
SILD Stack FM-4 konformer Monitoring-Stack (HL7 v2 · FHIR R4 · Prometheus · Grafana) github.com/fmatten/SILD
AION FM-3: Algebraic Interval Ontology for Clinical Networks github.com/fmatten/aion · codeberg.org/iscad/aion · 10.5281/zenodo.19553130

Contributing

Contributions are welcome under AGPL-3.0 OR Commercial. 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 = {AGPL-3.0-only},
  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.4.tar.gz (129.3 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.4-py3-none-any.whl (65.8 kB view details)

Uploaded Python 3

File details

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

File metadata

  • Download URL: cairn_clinical-1.0.4.tar.gz
  • Upload date:
  • Size: 129.3 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.4.tar.gz
Algorithm Hash digest
SHA256 6e51920fd4c22e754d7ccdba7459db563bea134b3c749408a4558b2c174f389d
MD5 634be4d40f4727776d9531435740ab28
BLAKE2b-256 96124bd826bb08bbc0653e408b1698fa402c0609ac1b867756bd92818e865d1d

See more details on using hashes here.

File details

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

File metadata

  • Download URL: cairn_clinical-1.0.4-py3-none-any.whl
  • Upload date:
  • Size: 65.8 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.4-py3-none-any.whl
Algorithm Hash digest
SHA256 693beff8726b6db348facfbf363c88b2c0f9ec35d27eb4874d7b5d2ebccba047
MD5 58a709969dc9f675d3c451bff7c4af2e
BLAKE2b-256 78f2f174f9d2202e6b21a32fc26b0a774288f4c9edb9d813157fb0fbe4f63504

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