2026-04-01·9 min read·sota.io team

Deploy Isabelle to Europe — Formally Verified Software on EU Infrastructure in 2026

Most software is tested. Isabelle software is proved.

There is a fundamental difference. Tests check that a program does the right thing on the inputs you thought to try. Proofs check that a program does the right thing on every possible input — by mathematical necessity. Isabelle is a generic proof assistant: you state a theorem in higher-order logic, and Isabelle's kernel verifies that every step of your proof is logically valid. When the kernel says the proof is complete, there are no exceptions hiding in untested edge cases. The theorem holds.

The practical consequence of this was demonstrated in 2009 when NICTA (now Data61) completed the seL4 proof: a formally verified, mathematically proven, machine-checked proof that the seL4 microkernel correctly implements its specification and that the C source code correctly implements the design. It was the first full formal verification of a production operating system kernel. SeL4 now runs in avionics, automotive, and defence systems. The proof was done in Isabelle/HOL.

On sota.io's EU infrastructure, verified code extracted from Isabelle proofs runs in Germany. Safety certificates, formal specifications, and verified executables remain under EU jurisdiction — precisely where the EU AI Act and GDPR require them to be.

Lawrence Paulson and Tobias Nipkow

Lawrence Paulson 🇬🇧 is a Professor of Computational Logic at the University of Cambridge Computer Laboratory. He designed Isabelle in 1986 and released the first version in 1988. Paulson's background was in the LCF tradition — the Logic for Computable Functions system developed by Robin Milner at Edinburgh and later Cambridge in the 1970s, which introduced the idea of an ML meta-language for expressing proofs. Isabelle extended the LCF approach into a generic theorem prover: rather than being committed to a single logic, Isabelle could host multiple object logics (FOL, HOL, ZF, and others) within a single logical framework called the Isabelle meta-logic.

Paulson also proved the Consistency of the Constructive Type Theory and formalised many number-theoretic results in Isabelle, including work on cryptographic protocol verification that became the foundation for formal security proofs of TLS and authentication protocols used across EU e-government systems.

Tobias Nipkow 🇩🇪 is a Professor of Computer Science at Technische Universität München (TUM). From the early 1990s, Nipkow developed Isabelle/HOL — the Higher-Order Logic instantiation of Isabelle that became, and remains, the most widely used variant. His textbook Concrete Semantics (2014, with Gerwin Klein) is the standard reference for mechanised semantics, and the entire book is formalised in Isabelle — every theorem in the text has a machine-checked proof. TU Munich is one of the strongest centres of formal methods research in Europe, and Nipkow's group has produced much of the Isabelle infrastructure that the global community depends on today.

Markus Wenzel 🇩🇪, formerly TU Munich and now at various European institutions, designed the Isar proof language — the structured, document-oriented proof notation that replaced tactic scripts in modern Isabelle development. Isar proofs read like mathematical textbook proofs: structured with show, have, hence, thus keywords that make the proof's logical skeleton visible to human readers. This readability is directly relevant to regulatory contexts where proofs must be reviewed by auditors.

What Makes Isabelle/HOL Distinctive

The LCF Architecture: Small Kernel, Total Correctness

Isabelle follows the LCF architecture: a small, trusted kernel verifies every inference step. No matter how complex the tactic, the term rewriter, or the automation, every proof obligation eventually reduces to primitive inferences verified by the kernel. If the kernel accepts the proof, it is correct. The kernel is small enough to be manually audited — this is the root of trust.

(* Every proof step reduces to kernel-verified primitive inferences *)
(* The kernel implements only these basic rules: *)

(* Modus Ponens: if ⊢ P → Q and ⊢ P then ⊢ Q *)
theorem modus_ponens: "P → Q ⟹ P ⟹ Q"
  by (rule mp)

(* Universal instantiation: if ⊢ ∀x. P x then ⊢ P t *)
theorem universal_inst: "∀x. P x ⟹ P t"
  by (rule spec)

This design means that bugs in Isabelle's automation, decision procedures, or tactic libraries cannot silently produce false theorems. A buggy tactic produces a failed proof, not an accepted falsehood.

Isabelle/HOL: Higher-Order Logic for Software Verification

Higher-Order Logic allows quantification over functions and predicates, not just first-order variables. This expressiveness makes it possible to state and prove theorems about programs directly — program functions become HOL functions, data types become HOL types, and correctness properties become HOL theorems.

(* GDPR-compliant data processing: prove that anonymisation 
   removes all direct identifiers before statistical processing *)

datatype personal_record = Record (name: string) (email: string) 
                                  (iban: string) (value: real)

(* Anonymisation: replace PII fields with constant markers *)
definition anonymise :: "personal_record ⇒ personal_record" where
  "anonymise r = Record ''[REDACTED]'' ''[REDACTED]'' ''[REDACTED]'' (value r)"

(* Theorem: anonymised record contains no personal identifiers *)
(* (formalises GDPR Art. 4(5) pseudonymisation requirement) *)
theorem anonymise_removes_pii:
  "name (anonymise r) = ''[REDACTED]'' ∧
   email (anonymise r) = ''[REDACTED]'' ∧
   iban (anonymise r) = ''[REDACTED]''"
  by (simp add: anonymise_def)

(* Statistical aggregate: sum of values — no PII in output *)
definition aggregate_values :: "personal_record list ⇒ real" where
  "aggregate_values rs = sum_list (map value rs)"

(* Privacy-preserving pipeline: anonymise all records, then aggregate *)
definition gdpr_safe_sum :: "personal_record list ⇒ real" where
  "gdpr_safe_sum rs = aggregate_values (map anonymise rs)"

(* Proof: aggregate is identical on raw and anonymised records *)
(* (the aggregation does not leak PII through its result) *)
theorem gdpr_safe_sum_preserves_value:
  "gdpr_safe_sum rs = aggregate_values rs"
  by (simp add: gdpr_safe_sum_def aggregate_values_def)

Isar: Human-Readable Structured Proofs

Isar (Intelligible Semi-Automated Reasoning) proofs are structured like mathematical arguments in a textbook. Each step is explicitly labelled with what is being shown and how. This is not merely aesthetic: regulators reviewing AI system documentation or auditors verifying compliance implementations can read Isar proofs without Isabelle expertise.

(* EU AI Act Art. 15: Accuracy, robustness, and cybersecurity *)
(* Formal proof that a sorting algorithm is correct (stable, terminating) *)

theorem insertion_sort_correct:
  fixes xs :: "int list"
  shows "sorted (isort xs) ∧ set (isort xs) = set xs"
proof (induction xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  (* Inductive hypothesis: isort xs is sorted and set-equivalent *)
  have IH_sorted: "sorted (isort xs)" using Cons.IH by simp
  have IH_set: "set (isort xs) = set xs" using Cons.IH by simp
  (* Inserting x into a sorted list preserves sorted order *)
  have "sorted (ins x (isort xs))" using IH_sorted by (rule ins_sorted)
  (* The set of the result equals the set of the input *)
  moreover have "set (ins x (isort xs)) = {x} ∪ set (isort xs)"
    by (rule ins_set)
  (* Combining: isort (x # xs) meets both requirements *)
  ultimately show ?case using IH_set by (simp add: isort_def)
qed

Code Extraction: Verified Haskell and Standard ML

Isabelle/HOL can extract functional programs from verified specifications. The extracted code inherits the proof's correctness guarantee: if you proved that the specification is correct, the extracted program implements the specification, by construction.

(* Verified EU financial calculation: correct rounding for MiFID II *)

(* Specification: round half-up to N decimal places *)
definition round_halfup :: "nat ⇒ real ⇒ real" where
  "round_halfup n x = real_of_int (⌊x × 10^n + 0.5⌋) / 10^n"

(* Theorem: idempotent — rounding twice gives same result *)
theorem round_halfup_idempotent:
  "round_halfup n (round_halfup n x) = round_halfup n x"
  sorry (* proof omitted for space — would use floor properties *)

(* Export to executable Haskell for deployment *)
export_code round_halfup in Haskell
  module_name MiFID.Rounding
  file_prefix mifid_rounding

The exported Haskell file compiles with GHC and deploys on any Linux server — including sota.io's EU infrastructure in Germany.

Deploy Isabelle on sota.io

Isabelle ships a server mode (isabelle server) that accepts commands over TCP and returns structured JSON responses. Combined with a thin HTTP wrapper, Isabelle can serve as a backend formal verification service.

Prerequisites

sota.io account (sign up at sota.io)
Docker installed locally
An Isabelle theory file (.thy) containing your verified algorithms

Step 1 — Project Structure

mkdir eu-isabelle-api
cd eu-isabelle-api

ls
# Rounding.thy         — Isabelle theory with verified algorithms
# server.py            — HTTP wrapper for Isabelle server
# Dockerfile
# sota.json

Step 2 — Isabelle Theory

(* Rounding.thy — verified MiFID II rounding for EU financial services *)
theory Rounding
  imports Main HOL.Real
begin

(* Round a real number to N decimal places using half-up rule *)
definition round_halfup :: "nat ⇒ real ⇒ real" where
  "round_halfup n x ≡ real_of_int (⌊x × (10 ^ n) + 1/2⌋) / (10 ^ n)"

(* Theorem: result is always a valid decimal with N places *)
theorem round_halfup_range:
  fixes x :: real and n :: nat
  assumes "x ≥ 0"
  shows "∃k :: int. round_halfup n x = real k / (10 ^ n) ∧ k ≥ 0"
  unfolding round_halfup_def
  by (auto intro: exI[of _ "⌊x × (10 ^ n) + 1/2⌋"] simp: divide_nonneg_nonneg)

(* Code export: extract verified Haskell implementation *)
export_code round_halfup in Haskell
  module_name MiFID.Rounding

end

Step 3 — HTTP Wrapper

# server.py — thin HTTP wrapper around Isabelle verification service

import subprocess
import json
import os
from http.server import HTTPServer, BaseHTTPRequestHandler

class IsabelleHandler(BaseHTTPRequestHandler):
    def do_POST(self):
        if self.path == "/verify":
            length = int(self.headers["Content-Length"])
            body = json.loads(self.rfile.read(length))
            theory = body.get("theory", "")
            
            # Write theory to temp file and run Isabelle check
            with open("/tmp/Check.thy", "w") as f:
                f.write(theory)
            
            result = subprocess.run(
                ["isabelle", "process", "-T", "/tmp/Check.thy"],
                capture_output=True, text=True, timeout=60
            )
            
            response = {
                "verified": result.returncode == 0,
                "output": result.stdout[-2000:],  # last 2000 chars
                "region": "EU-DE",
                "gdpr_compliant": True
            }
            
            self.send_response(200)
            self.send_header("Content-Type", "application/json")
            self.end_headers()
            self.wfile.write(json.dumps(response).encode())
        else:
            self.send_response(404)
            self.end_headers()

    def log_message(self, format, *args):
        pass  # suppress access log noise

if __name__ == "__main__":
    port = int(os.environ.get("PORT", "8080"))
    print(f"Isabelle verification service on :{port} (EU-DE)")
    HTTPServer(("0.0.0.0", port), IsabelleHandler).serve_forever()

Step 4 — Dockerfile

FROM debian:bookworm-slim

# Install Java (Isabelle requires JVM) and Python
RUN apt-get update && apt-get install -y --no-install-recommends \
    openjdk-17-jre-headless curl python3 \
    && rm -rf /var/lib/apt/lists/*

# Download and install Isabelle (Isabelle2024)
RUN curl -fsSL https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz \
    -o /tmp/isabelle.tar.gz \
    && tar -xzf /tmp/isabelle.tar.gz -C /opt \
    && ln -s /opt/Isabelle2024/bin/isabelle /usr/local/bin/isabelle \
    && rm /tmp/isabelle.tar.gz

# Build Isabelle session heap (HOL, first startup is slow)
RUN isabelle build -b HOL 2>/dev/null || true

# Application
RUN addgroup --system isabelle && adduser --system --ingroup isabelle isabelle
WORKDIR /app
COPY Rounding.thy server.py ./

USER isabelle
EXPOSE 8080
CMD ["python3", "server.py"]

Step 5 — sota.json Configuration

{
  "name": "eu-isabelle-verifier",
  "region": "eu-central",
  "memory": "2GB",
  "database": {
    "engine": "postgresql",
    "version": "17"
  },
  "env": {
    "ISABELLE_HOME": "/opt/Isabelle2024",
    "DATA_RESIDENCY": "EU-DE"
  }
}

Step 6 — Deploy to EU Infrastructure

# Deploy Isabelle verification service to Hetzner Germany
sota deploy

# Output:
# Building Docker image...
# Deploying to Hetzner Germany (eu-central)...
# TLS certificate provisioned
# Service running at https://your-isabelle.sota.io
# Region: EU (Germany) — GDPR-compliant by default

# Test: verify a simple theorem
curl -X POST https://your-isabelle.sota.io/verify \
  -H "Content-Type: application/json" \
  -d '{"theory": "theory Test imports Main begin\nlemma \"1 + 1 = (2::nat)\" by simp\nend"}'
# {"verified": true, "output": "...", "region": "EU-DE", "gdpr_compliant": true}

Isabelle and EU Compliance

EU AI Act — Article 9 and Article 15

The EU AI Act imposes the strictest obligations on high-risk AI systems (Annex III: biometric systems, credit scoring, employment screening, critical infrastructure management). Article 9 requires a documented risk management system. Article 15 requires accuracy, robustness, and cybersecurity measures throughout the system lifecycle.

Isabelle formal proofs address the core of both requirements:

Article 9 risk management: documented proofs that algorithms behave correctly at all inputs — not merely tested, but mathematically certified
Article 15 accuracy: machine-checked proofs of numerical correctness (rounding, precision, overflow bounds) for financial and actuarial calculations
Article 15 robustness: proofs of invariant preservation under adversarial inputs — no edge case can violate the proved property
Audit trail: Isabelle proof documents are machine-readable, version-controlled, and independently verifiable — any third party can re-run the verification

(* EU AI Act Art. 15 — robustness: credit scoring model *)
(* Proof that score is always in [0, 1000] regardless of input *)

definition credit_score :: "applicant ⇒ nat" where
  "credit_score a = clamp 0 1000 (base_score a + history_bonus a)"

theorem credit_score_bounded:
  "∀ a. credit_score a ≥ 0 ∧ credit_score a ≤ 1000"
  by (simp add: credit_score_def clamp_def)

GDPR Articles 5 (data minimisation), 25 (privacy by design), and 89 (pseudonymisation for research) can be satisfied not merely by policy but by proof:

Article 5(1)(c) data minimisation: prove that an algorithm's output contains no more personal data than necessary for the specified purpose
Article 25 privacy by design: prove that a data pipeline never exposes a PII field to an output or log outside the permitted scope
Article 89 safeguards for statistical processing: prove that aggregate statistics cannot be used to reconstruct individual records (differential privacy lower bounds)

Formal proofs make GDPR compliance auditable beyond policies and procedures: a Data Protection Officer can commission independent verification of the correctness proof rather than trusting an internal review.

DO-178C — Avionics and Safety-Critical Systems

DO-178C (Software Considerations in Airborne Systems) requires rigorous evidence of software correctness for aviation certification. Level A software (catastrophic failure category) requires the most stringent evidence. Isabelle-verified code satisfies the "formal methods supplement" pathway in DO-178C, which reduces the number of required test cases in exchange for machine-checked correctness proofs.

The CompCert certified C compiler — itself verified in Rocq/Coq — has demonstrated this pathway in the Airbus supply chain. Isabelle-verified algorithms extracted to Haskell or Standard ML, compiled through verified compilers, produce trusted executables for EU aerospace programs.

NIS2 — Critical Infrastructure Security

NIS2 (Directive 2022/2555/EU) requires operators of essential services — energy grids, water systems, financial market infrastructure, healthcare — to implement systematic risk management and demonstrate appropriate security measures. For software components in NIS2-critical systems, Isabelle proofs provide:

Absence of buffer overflows: proved bounds on array accesses
No integer arithmetic overflows: proved range invariants for safety-critical calculations
Correct cryptographic protocol behaviour: Paulson's original protocol verification work in Isabelle has been applied to formal analysis of authentication and key exchange protocols used across EU network infrastructure

European Roots and Global Impact

Isabelle's development is one of the great collaborative products of European academic computing:

Lawrence Paulson 🇬🇧 — University of Cambridge Computer Laboratory. Designed Isabelle in 1986–1988 from the LCF tradition of Edinburgh and Cambridge. Proved the consistency of number theory and the cryptographic correctness of TLS-style protocols in Isabelle.
Tobias Nipkow 🇩🇪 — Technische Universität München. Developed Isabelle/HOL from the early 1990s. Co-author of Concrete Semantics (the full textbook is formalised in Isabelle). Member of the German Academia Leopoldina.
Markus Wenzel 🇩🇪 — Designed the Isar proof language, making Isabelle proofs readable as mathematical documents. Worked at TU Munich and at various European research institutions.
Stefan Berghofer 🇩🇪 — TU Munich. Contributed significant infrastructure including the code generator that enables Haskell and Standard ML extraction.
Jasmin Blanchette 🇫🇷/🇩🇪 — Inria Paris and VU Amsterdam. Developed Sledgehammer (automated proof search via SMT solvers and first-order provers) and Nitpick (counterexample finder). Modern Isabelle users rely on these tools for nearly every non-trivial proof.
Gerwin Klein 🇩🇪 — TU Munich and NICTA/Data61. Led the seL4 formal verification project — the proof that made Isabelle famous outside theorem prover communities.
Archive of Formal Proofs — Maintained by the Isabelle community, predominantly European. Over 700 peer-reviewed entries covering number theory, algebra, graph algorithms, cryptography, data structures, and concurrent program verification.

The Isabelle heritage connects Cambridge, Munich, and a network of European universities and research institutes. Its industrial impact is visible in avionics (seL4 in Airbus suppliers), financial infrastructure (formally verified protocol implementations), and the formal methods curricula at TU Munich, ETH Zurich, TU Berlin, Uppsala, and Chalmers.

Why sota.io for Isabelle

EU-native infrastructure: Hetzner Germany. Your formal verification service, extracted verified code, and proof artifacts all stay under EU jurisdiction — matching the regulatory requirements that motivated the formal verification in the first place.

Simple deployment: sota deploy from your project directory. Isabelle runs in a standard Debian container with OpenJDK. No Isabelle-specific platform configuration required.

Flat-rate pricing: €9/month for 2 GB RAM, 2 vCPU, managed PostgreSQL. Isabelle's JVM requires more memory than a typical service, but 2 GB is sufficient for most verification workloads in server mode.

Managed PostgreSQL: Store proof results, verification certificates, and compliance audit logs in EU-sovereign PostgreSQL 17 with automated backups. ISO 27001 certified infrastructure.

Compliance documentation: Isabelle proofs are machine-readable, version-controlled, and independently verifiable. They constitute the strongest possible evidence of software correctness for EU AI Act, GDPR, and DO-178C review. On sota.io, that evidence is produced and stored on EU-sovereign infrastructure.

Automatic TLS: HTTPS provisioned within seconds. Your formal verification API is secured by default.

See also: Deploy Lean 4 to Europe →, Deploy Agda to Europe →, Deploy Rocq (Coq) to Europe →, Deploy Haskell to Europe →, Deploy VDM-SL to Europe → — IBM Vienna Scientific Center 🇦🇹 (1970s), ISO/IEC 13817-1; VDM-SL's proof obligations are the formal targets that Isabelle/HOL can machine-verify for the highest-assurance EU safety-critical systems