ProvidEHR
Developer center · Lean 4 · red team · national-scale assurance

Inspect the architecture. Re-run the evidence. Challenge every boundary.

ProvidEHR is pursuing a rigorous, reproducible evidence standard for a population-prevention operating system and extensible longitudinal EHR foundation. Selected security-critical decisions are modeled in Lean 4; red-team and deterministic national-scale harnesses turn security and capacity claims into reviewable campaigns. This page distinguishes implemented harnesses from production-equivalent execution, independent review, and certification.

Inspect verified invariantsExplore architectureView source
Reproducible formal evidence
Evidence snapshot · 16 July 2026
Lean theorems
31 · exact public inventory
nanoda declarations
774 · independently checked closure
Rust scope combinations
131,072 · SMART closed-catalog table
complete canonical cases
24 · Lean-emitted SMART cases

17/17 claims map to checked Lean theorems. Tenant-model governance promotion still requires independent review; Rust refinement and production evidence remain 0/17.

Evidence vocabulary

These labels are intentionally not interchangeable.

Exercised
Implemented and supported by an executable test, rehearsal, or deployed non-PHI evidence path.
Implemented
Present in the codebase, with its activation and production evidence stated separately.
Sandbox
Available only behind explicit configuration, credentials, manual issuance, or non-production constraints.
Planned
A target-state design or work package; not represented as shipping capability.
Not claimed
Certification, scale, security, or operational evidence that ProvidEHR does not currently claim.
Lean 4 · independently checked formal evidence

Proof is a product feature—when its boundary is inspectable.

Thirty-one Lean theorem declarations cover the versioned SMART 1.0 model and the ninth formal protocol family for tenant/deployment-cell isolation. Every number below links model proof, independent checking, executable evidence, and known gaps without turning any one layer into a claim about the whole EHR.

providehr.smart 1.0.0 + providehr.tenant-isolation 1.0.0

Security-critical decisions are specified as proofs—not promises.

The current package contains checked Lean proofs for deliberately bounded SMART authorization and refresh decisions plus structural tenant/cell key and read isolation. It connects the SMART model to executable Rust evidence without relabeling conformance tests as refinement proof; the new runtime scope tests are still not a Lean-to-Rust refinement proof.

Evidence history: The original 22-theorem SMART snapshot remains intact. This release adds nine tenant and deployment-cell isolation theorems as protocol.tenant-isolation.v1, formal protocol family 09. Its two coverage claims map to kernel- and nanoda-checked Lean theorem terms, while formal-inventory model promotion remains withheld pending independent review. Rust property, differential, integration, refinement, and production evidence remain unpromoted. The combined 17-claim ladder preserves the historical SMART mapping without borrowing runtime credit for the new model.

Lean 4.31.0 · Rust 1.97.0 · pinned lean4export 3de59f10 · pinned nanoda 6524aed3 · allowlist: propext, Classical.choice, Quot.sound · sorryAx and compiler-trust primitives rejected

Pinned formal snapshot · c9a727e
Lean theorems
31
exact public inventory
nanoda declarations
774
independently checked closure
Rust scope combinations
131,072
SMART closed-catalog table
complete canonical cases
24
Lean-emitted SMART cases
narrow coverage claims
17
15 SMART + 2 tenant claims
model-bound source entries
34
24 unique paths; drift fails closed
Reproducible assurance chain

Proof term to production boundary, with every missing link visible.

8 explicit evidence stages
  1. 01

    Lean model

    Typed SMART decisions and structural tenant/cell storage decisions define a 31-theorem claim boundary.

  2. 02

    Lean kernel

    Lean 4.31.0 accepts the proof terms; separate release checks reject escape hatches.

  3. 03

    Exact export

    Pinned lean4export targets every theorem and fails if inventory drifts.

  4. 04

    Independent check

    Pinned nanoda accepts the 774-declaration closure and rejects sorryAx/compiler trust.

  5. 05

    Lean-emitted cases

    Lean emits 24 complete versioned inputs, outputs, grants, and state projections.

  6. 06

    Safe Rust kernel

    Property tables include 131,072 closed-scope combinations plus patient and refresh checks.

  7. 07

    Gateway evidence

    Named adapter regressions cover 10 of 17 claims; five SMART and two tenant-model gaps stay visible.

  8. 08

    Production boundary

    Rust refinement and production evidence remain 0 of 17; the tenant model does not change those zeroes by inference.

Scope safety

The model uses a closed seven-scope catalog, denies unknown scopes and inactive clients, contains grants within the registered client allowlist, and excludes direct-write scopes in enforce mode.

Patient isolation

Modeled Observation reads require the exact scope and patient binding. Sandbox writes require the matching patient and write scope; enforce mode denies every direct SMART write.

Replay resistance

Modeled refresh rotation requires the correct client and a fresh successor, consumes the presented token, rejects sequential replay, and preserves client, patient, and scopes.

Tenant/cell key isolation

The abstract storage model makes tenant and cell part of authoritative key identity. Different tenants or cells cannot alias, and reads with either coordinate mismatched return no value.

Complete public inventory

31 theorems. SMART plus tenant/deployment-cell isolation.

Helper lemmas are counted, named, exported, and independently checked—never folded into a vague “verified” badge.

Authorization and grants

Exact nonempty grants, active clients, closed scopes, allowlist containment, supported posture, and enforce-mode exclusion of direct-write scopes.

12
theorems
Inspect declaration inventory
  • ProvidEHRFormal.Smart.allScopes_true
  • ProvidEHRFormal.Smart.authorize_some_iff
  • ProvidEHRFormal.Smart.successful_grant_is_nonempty
  • ProvidEHRFormal.Smart.canGrant_compatible
  • ProvidEHRFormal.Smart.canGrant_active
  • ProvidEHRFormal.Smart.compatible_allows
  • ProvidEHRFormal.Smart.compatible_supports
  • ProvidEHRFormal.Smart.granted_scopes_subset_client_allowlist
  • ProvidEHRFormal.Smart.successful_grant_uses_only_supported_scopes
  • ProvidEHRFormal.Smart.enforce_grants_have_no_direct_write
  • ProvidEHRFormal.Smart.unknown_scopes_deny
  • ProvidEHRFormal.Smart.inactive_clients_deny

Direct-write posture

Enforce mode always denies direct SMART writes; a sandbox permit requires a direct-write scope and exact patient binding.

2
theorems
Inspect declaration inventory
  • ProvidEHRFormal.Smart.enforce_direct_writes_always_deny
  • ProvidEHRFormal.Smart.sandbox_write_permit_requires_scope_and_patient

Patient-bound reads

Modeled Observation reads require Observation.read and exact token-to-resource patient equality; explicit mismatch is denied.

2
theorems
Inspect declaration inventory
  • ProvidEHRFormal.Smart.observation_read_permit_requires_scope_and_patient
  • ProvidEHRFormal.Smart.observation_read_mismatched_patient_denied

Refresh rotation and replay

Correct-client rotation to a fresh successor consumes the presented token, preserves bindings, leaves denial state unchanged, and rejects replay.

6
theorems
Inspect declaration inventory
  • ProvidEHRFormal.Smart.rotate_success_iff
  • ProvidEHRFormal.Smart.successful_refresh_consumes_presented_token
  • ProvidEHRFormal.Smart.wrong_client_does_not_consume
  • ProvidEHRFormal.Smart.missing_refresh_is_denied
  • ProvidEHRFormal.Smart.successful_refresh_replay_fails
  • ProvidEHRFormal.Smart.successful_refresh_preserves_binding_and_scopes

Protocol family 09 · Tenant and deployment-cell isolation

Tenant and deployment-cell coordinates are part of authoritative key identity; differing scopes cannot alias, exact-scope reads preserve the selected value, and cross-tenant or cross-cell reads deny.

9
theorems
Inspect declaration inventory
  • ProvidEHRFormal.TenantIsolation.key_equality_preserves_tenant
  • ProvidEHRFormal.TenantIsolation.key_equality_preserves_cell
  • ProvidEHRFormal.TenantIsolation.tenant_difference_prevents_key_alias
  • ProvidEHRFormal.TenantIsolation.cell_difference_prevents_key_alias
  • ProvidEHRFormal.TenantIsolation.scope_difference_prevents_key_alias
  • ProvidEHRFormal.TenantIsolation.exact_scope_read
  • ProvidEHRFormal.TenantIsolation.cross_scope_read_denied
  • ProvidEHRFormal.TenantIsolation.cross_tenant_read_denied
  • ProvidEHRFormal.TenantIsolation.cross_cell_read_denied
Coverage-manifest claim evidence

Proved where the model reaches. Explicit where it stops.

Lean theorem terms checked

17/17

All 15 SMART and 2 tenant-isolation claims name checked theorems; tenant governance promotion awaits independent review.

Rust property tested

15/17

All SMART claims are covered; both tenant-model claims remain unpromoted.

Differential tested

14/17

One SMART replay trace and both tenant-model claims remain outside versioned cross-language fixtures.

Rust refinement proved

0/17

No theorem connects the production Rust implementation to the Lean functions.

Integration tested

10/17

Five SMART adapter contracts and both tenant-model claims retain explicit gaps.

Production evidenced

0/17

Model evidence is not represented as deployed operational evidence.

Representative enforce-mode invariant
Lean 4
theorem enforce_grants_have_no_direct_write {client : Client}
    {request : AuthorizationRequest} {grant : Grant}
    (hauthorize : authorize .enforce client request = some grant)
    (scope : Scope) (hgranted : grant.scopes scope = true) :
    isDirectWrite scope = false := by
  have hsupported := successful_grant_uses_only_supported_scopes
    hauthorize scope hgranted
  cases scope <;> simp_all [isSupported, isDirectWrite]
Re-run the verification

Pinned toolchains, exact inventories, complete-case comparison, and source-drift checks are repository-owned gates.

$ (cd formal/lean && lake build ProvidEHRFormal && lake env leanchecker ProvidEHRFormal.Smart && lake env leanchecker ProvidEHRFormal.TenantIsolation)
$ scripts/verify-formal-nanoda.sh
$ cargo test -p protocol-kernel --locked
$ scripts/verify-formal-vectors.sh
$ scripts/verify-formal-coverage.sh
Lean SMART modelLean tenant/deployment-cell isolation modelCoverage ledgerFormal specification inventoryCanonical casesSafe Rust kernelTenant runtime scope typesScoped store boundary testsRust property tablesIndependent checker gatePinned verification workflowFormal verification boundary

Where the current proof stops

  • The production Rust adapter is not refinement-proved equivalent to the Lean functions
  • SurrealDB row/query isolation, database credential cutover, persistence, concurrency, restart, or infrastructure
  • Cryptography, HTTP parsing, identity proofing, or correct vendor and network behavior
  • Every FHIR resource, clinical protocol, AI behavior, medical outcome, or regulatory requirement
  • That a single-node release is highly available, population-scale, or certified

Next proof waves

  1. 01SurrealDB row/query scoping, credential cutover, and runtime conformance evidence for the tenant model
  2. 02Consent event ordering, exact idempotency, withdrawal, and durable CAS
  3. 03Delegation attenuation, tenant binding, expiry, and revocation
  4. 04Atomic action-grant and clinician-attestation consumption
  5. 05Versioned audit digests and persistent-chain parity
  6. 06Trial correction history, IRT reconciliation, deterministic export, and restart/restore
  7. 07MPI merge/unmerge reversibility and identifier consistency
  8. 08Order, result, note, medication, agent write-back, and interoperability state machines
Hosted CI boundary: Local proof and evidence gates pass. Hosted Actions is not shown as passing because repository billing/spending currently prevents runner allocation; affected jobs executed zero steps.

One canonical clinical record

Versioned openEHR-compatible compositions remain the authoritative ProvidEHR record. FHIR, IPS, registry, OMOP, MCP, A2A, analytics, and UI views are controlled projections or workflow surfaces—not parallel clinical databases.

Policy before effects

On migrated high-risk mutation paths, verified identity, tenant, role and patient scope, purpose and consent context, capability, and approval evidence are evaluated before effect. Coverage remains path-specific until one adjudicator governs every REST, FHIR, export, MCP, A2A, and integration path. Agent output must not become authoritative merely because a model produced it.

Bounded co-work

Codex, Claude Code, Claude Cowork, MCP, and A2A receive typed capabilities and short-lived delegated context. They do not receive raw database access or an unrestricted FHIR write primitive.

Claims follow evidence

Implemented, exercised, sandbox, planned, and not-claimed states stay distinct. A Lean theorem proves its model; it does not silently become a claim about all Rust, infrastructure, clinical outcomes, or certification.

Adversarial security + national-scale validation

Two versioned assurance contracts. No borrowed confidence.

ProvidEHR now versions the methods needed to test hostile behavior and an exact 10,000,000-patient, 20-cell engineering target. Implementing a harness is the beginning of evidence: production-equivalent execution, failure and restore phases, and independent review are separate promotion gates.

Implemented

Adversarial security assurance

Make control failure reproducible before an attacker makes it consequential.

Implemented evidence machinery
  • A versioned attack catalog covers authorization, tenant/cell isolation, SMART replay, database authority, audit, consent/policy, MCP/A2A, integration, fuzzing, DAST, and evidence integrity.
  • A bounded no-shell orchestrator verifies exact sources, time limits, concurrency, evidence hygiene and deterministic selection.
  • Mutation tests deliberately weaken controls and evidence so a silent or decorative gate fails the suite.
Required before promotion
  • Execute the complete release and scheduled profiles in an isolated ephemeral runner.
  • Retain approved fuzz/DAST outputs and safe reproducers under the evidence policy.
  • Complete independent penetration testing and remediate findings before a promoted security claim.
Read the red-team assurance contract
Implemented

National-scale performance and integrity assurance

Engineer toward 10,000,000 patients—and make the word validated expensive.

Implemented evidence machinery
  • An exact national profile targets 10,000,000 de-identified synthetic patients across 20 isolated deployment cells: 500,000 identities per cell.
  • Deterministic constant-memory generation and reconciliation make expected identifiers, counts and digests reproducible without materializing the population in memory.
  • Remote execution is opt-in and evidence distinguishes the target profile from the workload actually completed.
Required before promotion
  • Run the full workload on production-equivalent multi-cell infrastructure with distributed load generators.
  • Complete soak, headroom, dependency failure, restart, restore and corruption-reconciliation phases.
  • Have an independent party review the benchmark method, raw telemetry and content-hashed, revision-bound evidence report.
Read the national-scale assurance contract
Current claim boundary: the national profile and assurance harnesses are implemented. ProvidEHR does not yet claim a production-equivalent 10M result, national rollout readiness, HA/DR, penetration resistance, medical-product certification, or comparative market superiority.
Architecture · code-versioned diagrams

C4 context, containers, UML sequences, and control flows.

Each visual is generated client-side from a static repository definition. The server-rendered text version is the accessible source of truth and survives disabled JavaScript or renderer failure.

Implemented
C4 context

Population prevention system context

COSMIC remains the incumbent EHR; ProvidEHR adds prevention workflows and a governed record; InVivo closes the between-visit patient loop.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. Patients use InVivo for CarePlan follow-through and consented between-visit evidence.
  2. Clinicians review and attest through the ProvidEHR workspace.
  3. Codex and Claude co-work enter through delegated MCP or bounded skills, never the database.
  4. ProvidEHR applies identity and policy before clinical capabilities reach the versioned record.
  5. Cambio COSMIC remains authoritative for incumbent workflows while adapter work is activation-gated.
  6. Swedish national services are an explicit integration path; complete live connectivity is not claimed.

Boundary: The diagram expresses component responsibility. It does not claim that every Swedish national connector or COSMIC sandbox workflow is live.

Exercised
Container

Runtime containers and trust boundaries

Browsers and agents terminate at controlled APIs. Only Rust services access the clinical store; integration credentials are mounted into isolated workers.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. The web application and agent clients call the HTTPS edge.
  2. The Rust gateway starts with a validated, server-selected tenant and deployment-cell scope; no default scope is available.
  3. The gateway authenticates the caller and resolves capability context inside that immutable runtime scope.
  4. Clinical effects use typed services, staging, and approval rather than browser-to-database access.
  5. SurrealDB stores the versioned record and operational state behind Rust services.
  6. A separate worker reads mounted credentials and derives the same tenant/cell scope before external delivery.

Boundary: Runtime scope is explicit, but complete SurrealDB row/query isolation and deployed credential cutover are not yet claimed. The locally exercised evidence environment is single-node; clustered failover, regional cells, and durable distributed delegation remain target-state work.

Exercised
UML sequence

SMART authorization and patient-bound read

The implemented standalone launch uses registered clients, exact redirect and scope allowlists, PKCE, patient binding, and enforce-mode read-only posture.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. The app requests a pre-registered redirect, scopes, and PKCE challenge.
  2. ProvidEHR rejects unknown clients, redirects, scopes, and scope escalation before login.
  3. The patient sees and approves the exact scope set.
  4. Code exchange verifies PKCE and returns patient- and client-bound credentials.
  5. Each FHIR read revalidates the live client, token, scope, and exact patient.
  6. Refresh tokens rotate on use; wrong-client attempts do not consume them and replay is denied.

Boundary: Codes, pending requests, and refresh families are currently process-local. EHR/workforce launch, durable revocation, and sender-constrained tokens remain planned.

Implemented
UML sequence

Governed draft-to-authoritative write

Implemented staging and promotion controls show the intended common write boundary for UI, FHIR, MCP, A2A, and integrations.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. An agent or integration proposes a typed draft with source references.
  2. Policy evaluates caller, patient, tenant, purpose, consent, and requested action.
  3. Permitted output lands in staging with an immutable hash and explicit must-review regions.
  4. A credentialed clinician reviews the exact version and signs an attestation.
  5. Promotion verifies identity, key status, content hash, version, and single-use approval evidence.
  6. The authoritative composition and audit evidence are committed through controlled services.

Boundary: Staging and promotion are implemented, but not every REST, FHIR, MCP, A2A, or integration mutation has yet been migrated behind one durable adjudicator.

Sandbox
Control flow

Codex and Claude co-work boundary

One repository plugin packages shared healthspan skills while each host receives an explicit, least-privilege connection profile.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. The repository marketplace exposes a validated ProvidEHR Healthspan Co-work plugin.
  2. Codex and Claude hosts receive the same bounded skills and capability documentation.
  3. Local Codex uses a short-lived environment token and a read-oriented tool allowlist.
  4. Claude Code and Cowork inject a sensitive plugin option into the remote MCP connection.
  5. The MCP server resolves delegation before exposing clinical capability results.
  6. Hosted Codex Work/ChatGPT PHI access is disabled until an OAuth/app connector exists.

Boundary: The plugin is installable; customer identity issuance, enterprise installation policy, durable delegation, and hosted OAuth remain production gates.

Sandbox
Control flow

Release, restore, and scale-out evidence

Repository evidence includes a deterministic local export/import/restart rehearsal. Multi-node and regional disaster recovery are deliberately shown as unproven next steps.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. Start from an immutable application release identifier.
  2. Export clinical state with checksums and import it into an isolated database.
  3. Restart the database and API rather than validating only an in-process restore.
  4. Reconcile record counts and controlled reads against the source evidence.
  5. Retain the rehearsal output as operational evidence.
  6. Automated encrypted backups, multi-node failover, and regional recovery remain planned and unclaimed.

Boundary: A single-node restore rehearsal is not high availability, an agreed RPO/RTO, or regional disaster-recovery evidence.

Implemented
Control flow

Red-team evidence pipeline

A versioned attack catalog drives bounded runners, security tools, mutation checks, retained reproducers, and release decisions without treating a scanner invocation as a penetration test.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. Map requirements and hazards to explicit threats and abuse cases.
  2. Select exact versioned attacks from the repository catalog.
  3. Run bounded authorization, tenant, SMART, parser, database, fuzzing, and DAST jobs in an isolated ephemeral environment.
  4. Normalize results into PHI-free evidence while retaining safe deterministic reproducers.
  5. Use mutation tests to prove that required controls and gates detect deliberate weakening.
  6. Hash the evidence manifest and require a release decision plus independent review for promoted claims.

Boundary: The catalog, verifier, bounded runner, and mutation tests are implemented. A complete release and scheduled campaign, retained external-tool evidence, and an independent penetration test remain required before claiming penetration resistance.

Planned
Control flow

Phase-separated national-scale acceptance design

The target acceptance design covers 10,000,000 deterministic synthetic patients across 20 isolated deployment cells, with load, failure, restore, and integrity phases producing one reconciled evidence report.

Visual loads as this section approaches the viewport

Text version and assurance boundary
  1. Lock the exact national profile at 10,000,000 synthetic patients across 20 isolated deployment cells.
  2. Generate deterministic de-identified identifiers and expected digests with constant-memory tooling.
  3. Run the representative prevention and longitudinal EHR workload through distributed generators.
  4. Exercise soak, N+1 headroom, degraded dependencies, restart, restore, and external-vendor failure.
  5. Reconcile per-cell counts, digests, duplicates, missing records, and cross-cell isolation against the locked corpus.
  6. Retain telemetry and a content-hashed, revision-bound report for an independently reviewed capacity decision.

Boundary: Profiles, deterministic generation and reconciliation, execution guardrails, and a local workload exercise are implemented. Full 20-cell fan-out, distributed generation, soak, dependency failure, restart/restore, N+1/failover tooling and execution, plus an independent benchmark, remain open acceptance gates.

Capability evidence

What exists, what has been exercised, and where it stops.

The matrix is release diligence, not a feature checklist. Every positive statement carries a boundary that prevents a broader reading.

AreaMaturityCurrent evidenceExplicit boundary
React clinician and marketing applicationsExercisedTanStack Start client and SSR builds, typed API clients, Vitest suites, and deployed HTTPS frontend.The browser is not a clinical database and keeps patient context out of persistent browser storage.
Rust clinical APIExercisedAxum services, focused authority and workflow tests, locked dependency builds, and broad local API test execution in the current evidence cycle.The backend code is implemented and exercised locally; a passing suite is not production deployment, penetration resistance, clinical certification, or population-scale capacity evidence.
Versioned clinical storeExercisedPersistent SurrealDB/RocksDB, version history, compositions, state transitions, and isolated export/import/restart rehearsal.SurrealDB 3.2.1 is pinned for the evidence environment. Production backend topology, managed storage, HA, DR, and cutover are not yet evidenced.
Tenant and cell runtime scopeImplementedStrict TenantId, CellId and DataScope values are mandatory at store construction; readiness, SMART configuration, audit evidence and in-memory durable-state keys preserve the same scope, with adversarial cross-scope tests.These tests are not promoted as formal Rust-property or refinement evidence. This runtime and in-memory foundation is not yet complete SurrealDB row/query isolation, proof that every application query is tenant-safe, or deployed multi-tenant evidence.
Runtime database authority and schema maintenanceExercisedThe API and worker use a record-authenticated runtime principal bound to an explicit authority generation; stale identities and owner-style runtime credentials fail closed. A separate maintenance controller and image owns schema preparation, provisioning, verification, and runtime-authority verification.The authority split is implemented and locally exercised. Production secret/KMS integration, deployed cutover, container-platform policy, transport controls, and independent operational evidence remain release gates.
openEHR, AQL, FHIR, IPS, and OMOP projectionsImplementedCanonical compositions plus controlled clinical, interoperability, registry, and analytics projections in Rust.Broad standard support is not the same as external certification or complete conformance-suite evidence.
SMART App LaunchExercisedRegistered clients, exact redirects/scopes, PKCE, signed patient-bound tokens, rotating refresh, and 30 focused regressions.Standalone patient launch only; enforce mode is read-only and durable refresh-family persistence is not complete.
Cambio COSMIC adapterSandboxTenant-bound connection contracts, inbound/outbound state, reconciliation, idempotent NEWS2 write-back, and fail-closed tests.Credentialed Cambio sandbox evidence and closure of current security gates are still required before activation.
Codex and Claude Co-work pluginImplementedRepository marketplace manifests, host-specific MCP configuration, shared skills, validation tests, and documented install flows.Hosted Codex Work/ChatGPT has no bundled OAuth/app connector for PHI; token issuance remains manual and short-lived.
MCP and A2A capability surfacesImplementedPublic non-PHI discovery, delegated clinical reads, typed tools/resources/prompts, A2A task execution, audit, and bounded registries.Durable A2A lifecycle, unified write approval, and broad agent write-back remain planned.
Lean protocol verificationExercisedLean 4.31.0 checks 31 theorems across the bounded SMART and tenant/cell-isolation models; nanoda independently checks 774 declarations; 24 complete SMART cases exercise safe Rust.The new isolation theorems prove the abstract scoped-key/read model. Production Rust is not refinement-proved equivalent, SurrealDB behavior is outside that model, and deployed operations are not proved.
Red-team assurance suiteImplementedA versioned attack catalog, bounded no-shell runner, exact-source verification, evidence-hygiene checks, attack profiles, and mutation tests make adversarial regressions reproducible.A complete isolated release/scheduled campaign, retained fuzz and DAST evidence, remediation review, and an independent penetration test have not yet been completed.
10M / 20-cell national-scale harnessImplementedAn exact 10,000,000-patient profile spans 20 isolated cells. Deterministic de-identified constant-memory corpus and reconciliation tools, guarded workload execution, profile verification, and a small local synthetic exercise are versioned.This is harness evidence—not a production-equivalent 10M result. The full run, soak/failure/restore campaign, HA/DR evidence, and independent benchmark remain unexecuted.
Regulated PHI production and medical-product classificationNot claimedA concrete target-state and release-gate backlog exists for IAM, tenant isolation, audit, DR, safety, quality, and regulatory evidence.ProvidEHR is not currently represented as certified, classified, highly available, or ready for unqualified regulated-PHI operation.
Security and assurance

Defense in depth, with the remaining controls visible.

ProvidEHR has real application controls and real gaps. Medical-product readiness requires both the implemented control plane and independently reviewable operational, safety, and quality evidence.

Identity and session

Implemented
  • Backend-owned users, organizations, memberships, clinical professions, and runtime privilege resolution
  • ES256 signed sessions and rejection of forged authority headers in enforce mode
  • Platform-only scopes for sensitive administration and integration operations
Next assurance gate

Generic OIDC/SAML federation, immutable issuer-subject accounts, SITHS/HSA assignments, session revocation, and key rotation evidence.

Clinical authorization

Implemented
  • Tenant, role/profession, patient, scope, purpose, consent, and capability checks on bounded paths
  • Patient-bound SMART reads and enforce-mode denial of direct authoritative SMART writes
  • Staged drafts, content hashes, clinician attestation, revocation checks, and single-use grants
Next assurance gate

One central policy decision and obligation engine enforced by every REST, FHIR, export, MCP, A2A, and integration path.

Data and audit

Sandbox
  • Versioned records, source references, audit events, bounded server-side indexes, and secret-free audit metadata
  • Mandatory tenant/cell runtime scope, scope-bound readiness and SMART configuration, store-bound audit evidence, and structurally scoped in-memory durable state
  • Record-authenticated runtime database authority is generation-fenced and separated from the offline schema-maintenance controller and image
  • Nonce-bound, 120-second runtime statements bind server-owned tenant/cell and release plus exact API, database, schema, deployment-manifest, and runtime-config digests to a current database-authority probe
  • Runtime statements use a versioned managed-provider signature receipt; incomplete configuration, stale database authority, receipt mismatch, and provider failure all fail closed
  • Managed identity signing moves session JWTs and collaboration release attestations to Vault Transit when completely configured, binds every request and receipt to tenant/cell/purpose/payload context, and locally verifies every P-256 signature against the configured public key before use
  • Managed SMART signing applies the same complete-or-fail Vault Transit boundary to SMART access tokens and OpenID ID tokens; JWKS publishes only the configured public key, and every versioned provider receipt and ES256 signature is locally verified before issuance
  • Managed SMART connector assertions keep RSA-3072/4096 private keys non-exportable in Vault Transit, bind every RS384 request and versioned receipt to tenant/cell/connector/token-endpoint context, locally verify signatures against configured SPKI bytes, and reject exportable PKCS#8 custody in production
  • Managed-provider audit reconciliation matches PHI-safe application expectations to normalized provider events by opaque request ID and exact key/version/algorithm/operation/outcome, failing closed on duplicates, missing evidence, unexpected successful use, denials, or metadata mismatch without retaining payloads, ciphertext, signatures, MACs, or resource context
  • Managed audit checkpoints sign the authoritative tenant/cell chain-head sequence and hash with an exact durable predecessor; replay is stable, stale predecessors are denied, and every persisted checkpoint is locally reverified so changed payloads fail closed
  • A locally contract-tested Vault Transit envelope provider authenticates canonical tenant/cell/purpose/resource/schema context, keeps AES-256-GCM keys non-exportable, and attributes both encryption and decryption to exact provider key versions
  • A dedicated managed HMAC-SHA-256 lookup provider includes the complete canonical runtime context in every token, preventing one identifier from correlating across tenants or purposes while attributing output to an exact non-exportable key version
  • The audit-only 1177 link is the first keyed-lookup consumer: complete configuration replaces enumerable hashes with tenant/cell/EHR/purpose-bound managed tokens; local no-provider records stay explicitly legacy and enforce mode remains blocked pending signed proofing
  • Managed ciphertext rewrap upgrades an available older envelope to the current AES key version under the identical authenticated context without returning plaintext, with exact source/result/provider receipts and fail-closed no-op or moved-context handling
  • Clinical store is accessed through Rust services, not Supabase or browser database clients
  • Release export/import/restart rehearsal and image/toolchain pinning
Next assurance gate

Complete application-query isolation coverage, migrate remaining protected persistence and identifier indexes to managed envelopes and keyed lookup, deploy Vault Transit and runtime authority in a production-equivalent cell, add signed national-identity proofing, wire live vendor credentials and complete external clinician-key lifecycle evidence, build durable resumable rewrap and dual-index MAC rotation with rollback and revocation, add connector public-key rollover and signing rotation, ingest live provider audit exports with alert delivery and operational reconciliation, publish checkpoints to externally custodied WORM storage and SIEM, independently verify managed runtime evidence, and add retention and legal hold.

Availability and assurance

Not claimed
  • Fail-closed runtime configuration and explicit activation gates
  • Unit, integration, differential, formal, dependency, client and SSR build gates, plus changed-surface lint checks
  • Versioned red-team and deterministic 10M/20-cell scale-assurance harnesses with claim-sensitive evidence boundaries
  • Documented current-versus-target architecture and release evidence boundaries
Next assurance gate

Production-equivalent 10M execution, soak/failure/restore, capacity SLOs, multi-node failover, encrypted offsite backups, agreed RPO/RTO, regional recovery, observability, independent benchmark and pen test, DPIA, safety case, QMS, and certification evidence.

Protocols and integrations

Standards are interfaces with maturity—not logos.

The current protocol portfolio supports a useful clinical slice. External certification, customer activation, national agreements, and full profile coverage remain separate evidence obligations.

openEHR REST + AQL

Canonical record, templates, compositions, versions, and controlled query

Implemented

Boundary: Compatibility is implemented; formal vendor conformance certification is not claimed.

FHIR R4/R5 + IPS

Clinical façade, patient-bound SMART access, documents, and interoperability projections

Implemented

Boundary: Not every resource, interaction, or national profile is complete.

SMART App Launch

Standalone patient authorization with PKCE and registered-client scope ceilings

Exercised

Boundary: No EHR/workforce launch; enforce-mode direct clinical writes are denied.

MCP 2025-11-25

Permissioned agent tools, resources, prompts, and source-cited clinical reads

Implemented

Boundary: Delegation issuance is short-lived; durable OAuth and broad governed writes remain incomplete.

A2A 1.0

Agent discovery, bounded skill execution, tasks, and artifacts

Implemented

Boundary: Task state is process-local and not yet a durable enterprise collaboration fabric.

Cambio COSMIC contracts

Tenant-bound patient matching, inbound sync, outbound delivery, reconciliation, and governed write-back

Sandbox

Boundary: Live credentialed sandbox validation remains an activation gate.

Swedish national ecosystem

1177/Journalen, NPÖ/HIE, SITHS/HSA, national terminology, quality registries, and EHDS alignment

Planned

Boundary: Strategy-aligned architecture and adapter plan; no blanket live-integration claim.

HL7 v2, C-CDA, X12, Bulk FHIR, FHIRcast, TEFCA/HIE

Target enterprise connector and exchange portfolio

Planned

Boundary: Roadmap scope, not current production capability.

Codex and Claude Co-work

Installable skills, bounded clinical context, human authority.

The same repository plugin serves Codex, Claude Code, and Claude Cowork. Host-specific authentication and tool exposure remain explicit so convenience never silently widens clinical authority.

Codex app, CLI, and IDE

Implemented
Install
Repository marketplace + providehr-healthspan plugin
Authentication
Short-lived PROVIDEHR_DELEGATION_TOKEN in the launching process
Boundary
Read-oriented tool allowlist; patient-report write is disabled in the Codex profile.

Claude Code

Implemented
Install
Repository marketplace or local --plugin-dir
Authentication
Sensitive plugin option injected as an HTTP bearer header
Boundary
Use a read-only delegation; replace the value after expiry or server restart.

Claude Cowork

Sandbox
Install
Git repository marketplace through Cowork → Customize → Plugins
Authentication
Sensitive plugin option and a publicly reachable MCP endpoint
Boundary
Anthropic cloud outbound access and customer installation policy must be validated.

Hosted Codex Work / ChatGPT

Not claimed
Install
Skills can be packaged; clinical connector is unavailable
Authentication
No hosted OAuth/app connector is bundled
Boundary
PHI-bearing MCP access must remain disabled on this surface.

Install for Codex

Issue delegation out of band and expose it only to the process that launches Codex.

$ codex plugin marketplace add advatar/ProvidEHR --ref main --sparse .agents/plugins --sparse plugins/providehr-healthspan
$ codex plugin add providehr-healthspan@providehr
$ codex plugin list

Install for Claude Code

Enable the intentionally disabled-by-default plugin, then supply a short-lived sensitive option.

$ claude plugin marketplace add advatar/ProvidEHR --sparse .claude-plugin plugins/providehr-healthspan
$ claude plugin install providehr-healthspan@providehr --scope user
$ claude plugin enable providehr-healthspan@providehr
Token handling: never commit, paste into documentation, or persist a clinical delegation token in a shell profile. Issue the minimum EHR/purpose/scope lifetime out of band and inject it through the host's sensitive option or launching process only.
Deployment and enterprise operations

A persistent data-plane implementation; a regional clinical service is the target.

The scale-out plan closes concrete availability, tenancy, security, observability, and assurance gaps. It is not used to relabel the locally exercised single-node evidence environment as a deployment.

Current

Current implemented and exercised codebase

  • Lovable-hosted React/TanStack application behind HTTPS
  • Rust API, worker and SurrealDB 3.2.1 data plane exercised locally
  • Record-authenticated, generation-fenced runtime database authority
  • Separate offline schema-maintenance controller and container image
  • Immutable configured tenant/cell scope across runtime services
  • Deterministic restore and small synthetic scale exercises—not continuous failover or a 10M result
Target

Regulated population-scale target

  • Regional cells with load-balanced stateless APIs and failure isolation
  • Clustered or managed data plane with storage-level tenant policy
  • Durable session, delegation, approval, queue, and audit state
  • Managed KMS/secrets, encrypted offsite backups, agreed RPO/RTO
  • OpenTelemetry, SLOs, load/chaos tests, on-call and release rollback
  • Production-equivalent 10M/20-cell campaign, independent benchmark and penetration test
  • DPIA, threat model, clinical safety case, QMS, and applicable certification evidence

Recovery

Restore, restart, reconcile, retain evidence; automate and add regional failover next.

Observability

Structured audit exists; distributed traces, capacity SLOs, and on-call evidence remain target state.

Supply chain

Toolchains, actions, and clinical images are pinned; expand SBOM, signing, provenance, and policy enforcement.

Governance

Separation of duties exists in bounded paths; complete tenant administration, safety, privacy, and QMS operations next.

Evidence library

Read the source decisions and operating boundaries.

Architecture diligence should end in versioned source, tests, ADRs, and release evidence—not an untraceable diagram deck.

Formal verification boundary

Theorem inventory, trusted base, assumptions, exclusions, and proof-to-code rule.

Target-state architecture

System responsibilities, interfaces, trust zones, data model, and phased target state.

Enterprise clinical platform plan

Work packages for charting, IAM, MPI, orders, medication, exchange, agents, DR, and certification readiness.

Co-work plugin contract

Codex and Claude installation, authentication boundaries, validation, and safe operating rules.

Architecture decisions

Versioned decisions for the canonical record, Rust-only store access, and governed agent capabilities.

Cambio prevention pitch

Complementary COSMIC, ProvidEHR, InVivo, and co-work responsibilities with explicit activation gates.

Red-team assurance contract

Versioned attack catalog, bounded execution, mutation gates, evidence hygiene, retained reproducers, and independent-review boundary.

National-scale assurance contract

Exact 10M/20-cell profile, deterministic corpus and reconciliation, workload phases, evidence manifest, and unexecuted production-equivalent gates.

Review the platform in context.

See the clinical workspace and prevention loop, or bring a security, architecture, interoperability, or clinical-safety diligence agenda to a working session.

Platform overviewRequest technical review