Deploy Nagini to Europe — Marco Eilers 🇩🇪 + ETH Zurich (2018), the Viper-Based Static Verifier for Python 3 Programs Used in AI Pipelines, Web Backends, and Data Processing, on EU Infrastructure in 2026

Python has become the language of artificial intelligence, data science, and scientific computing. FastAPI powers high-throughput web APIs, Django underpins enterprise platforms, NumPy and Pandas process financial and healthcare data, and TensorFlow and PyTorch train the models now subject to the EU AI Act. Python's accessibility is its greatest asset — and its greatest liability. Dynamic typing, aliasing, mutable shared state, and unchecked memory access make Python programs notoriously difficult to verify for correctness.

Nagini is a static verifier for Python 3 programs, developed at ETH Zurich 🇨🇭 (Eidgenössische Technische Hochschule) by Marco Eilers and Peter Müller, first published at VMCAI 2018 (Verification, Model Checking, and Abstract Interpretation). Nagini takes Python 3 source code annotated with preconditions, postconditions, loop invariants, and heap access specifications, translates it to the Viper intermediate verification language — also developed at ETH Zurich — and discharges proof obligations to Z3 via the Viper Silicon backend. The result is either a machine-checked correctness proof or a counterexample that pinpoints the specification violation.

Nagini completes the Viper ecosystem trilogy: Prusti (Rust, 2016/PLDI 2019), Gobra (Go, CAV 2021), and Nagini (Python, VMCAI 2018) cover the three dominant languages of modern software systems — all from ETH Zurich's Programming Methodology group under Professor Peter Müller, all sharing the same Viper verification infrastructure and permission-based heap model.

The Viper Ecosystem: One Backend for Three Languages

The insight behind the Viper project is that permission-based heap reasoning — Implicit Dynamic Frames (IDF) — provides a common model for memory access that fits multiple languages. Whether Rust's borrow checker, Go's pointer aliasing, or Python's reference semantics, the same Viper backend and the same Z3 SMT solver can discharge the resulting proof obligations.

Nagini was actually published before Gobra — VMCAI 2018 predates CAV 2021 by three years. The Viper ecosystem grew from Python (2018) through Rust (2019) to Go (2021), with Nagini establishing the proof-of-concept that Viper's permission model could handle a dynamically-typed language with objects and inheritance.

Nagini's Specification Language

Nagini specifications use function calls from the nagini_contracts library. Unlike Gobra (Go comments //@ ) or Prusti (Rust proc_macro attributes #[requires]), Nagini embeds specifications directly in Python code using ordinary Python syntax — the verifier intercepts these calls; the Python interpreter ignores them at runtime.

from nagini_contracts.contracts import *

def add(a: int, b: int) -> int:
    Requires(isinstance(a, int) and isinstance(b, int))
    Ensures(Result() == a + b)
    return a + b

Result() is a Nagini built-in referring to the function's return value. This is a complete functional correctness specification: for any two integers a and b, the function returns exactly a + b.

Preconditions, Postconditions, and Loop Invariants

from nagini_contracts.contracts import *

def factorial(n: int) -> int:
    Requires(n >= 0)
    Ensures(Result() >= 1)
    if n == 0:
        return 1
    result = 1
    i = 1
    while i <= n:
        Invariant(i >= 1 and i <= n + 1)
        Invariant(result >= 1)
        result = result * i
        i = i + 1
    return result

Invariant() inside a loop body establishes the inductive invariant. Nagini verifies that the invariant holds on entry, is preserved by each iteration, and implies the postcondition on exit.

Heap Access and Permission Logic

Python programs use objects with mutable fields. Nagini's permission model tracks which code currently holds read or write access to each object attribute:

from nagini_contracts.contracts import *

class Counter:
    def __init__(self) -> None:
        self.value = 0    # type: int
        Ensures(Acc(self.value))
        Ensures(self.value == 0)

    def increment(self) -> None:
        Requires(Acc(self.value))
        Ensures(Acc(self.value))
        Ensures(self.value == Old(self.value) + 1)
        self.value += 1

    def get(self) -> int:
        Requires(Acc(self.value, 1/2))
        Ensures(Acc(self.value, 1/2))
        Ensures(Result() == self.value)
        return self.value

Acc(self.value) — equivalent to Acc(self.value, 1/1) — is exclusive write permission. Acc(self.value, 1/2) is a fractional read permission; multiple concurrent readers may each hold 1/2, summing to the maximum 1. Old(expr) refers to the value of expr in the pre-state.

The permission model is Implicit Dynamic Frames: heap access permissions are implicit in the specification rather than explicit separation logic assertions, making specifications more readable while retaining the same verification power.

Object Invariants and Predicates

For complex data structures, Nagini supports Predicate definitions that encapsulate heap access and structural invariants:

from nagini_contracts.contracts import *
from typing import Optional, List

class LinkedList:
    def __init__(self) -> None:
        self.head = None    # type: Optional[Node]
        self.size = 0       # type: int

class Node:
    def __init__(self, val: int) -> None:
        self.val = val      # type: int
        self.next = None    # type: Optional[Node]

@Predicate
def list_inv(lst: LinkedList) -> bool:
    return (
        Acc(lst.head) and
        Acc(lst.size) and
        lst.size >= 0
    )

def append(lst: LinkedList, val: int) -> None:
    Requires(list_inv(lst))
    Ensures(list_inv(lst))
    Unfold(list_inv(lst))
    new_node = Node(val)
    if lst.head is None:
        lst.head = new_node
    lst.size += 1
    Fold(list_inv(lst))

Fold and Unfold convert between the abstract predicate and its concrete heap representation — the same Viper mechanism used in Gobra's fold/unfold operations.

Quantifiers: Specifying Properties Over Collections

from nagini_contracts.contracts import *
from typing import List

def sum_positive(items: List[int]) -> int:
    Requires(Acc(list_pred(items)))
    Requires(Forall(int, lambda i: (
        Implies(0 <= i and i < len(items), items[i] >= 0)
    )))
    Ensures(Acc(list_pred(items)))
    Ensures(Result() >= 0)
    total = 0
    idx = 0
    while idx < len(items):
        Invariant(Acc(list_pred(items)))
        Invariant(0 <= idx and idx <= len(items))
        Invariant(total >= 0)
        total += items[idx]
        idx += 1
    return total

Forall and Exists express universal and existential quantification over Python values. Here: "for all valid indices i, items[i] >= 0" — a precondition stating that all list elements are non-negative. The postcondition then follows: the sum of non-negative numbers is non-negative.

Thread Safety Verification

Python's Global Interpreter Lock (GIL) prevents true parallel execution for CPU-bound code, but I/O-bound Python programs do use threads, and Python 3.12's experimental no-GIL mode makes thread safety increasingly relevant. Nagini provides thread safety verification via Thread and Lock annotations:

from nagini_contracts.contracts import *
from threading import Thread, Lock

class SharedCounter:
    def __init__(self) -> None:
        self.value = 0      # type: int
        self._lock = Lock()

    def safe_increment(self) -> None:
        Requires(Acc(self.value) and Acc(self._lock))
        Ensures(Acc(self.value) and Acc(self._lock))
        self._lock.acquire()
        self.value += 1
        self._lock.release()

Nagini tracks lock ownership as a permission: acquire() transfers the lock's protected permission to the calling thread; release() transfers it back. Attempting to access a lock-protected resource without holding the lock produces a verification failure, not a runtime data race.

EU Regulatory Landscape: Python as Regulated Code

Python has evolved from a scripting language to the runtime substrate of regulated systems:

EU AI Act (2024) — High-Risk AI Systems

The EU AI Act (Regulation 2024/1689), applicable from 2026, places obligations on providers of high-risk AI systems (Annex III: medical devices, critical infrastructure, employment decisions, law enforcement). Article 9 mandates a risk management system that includes verification and validation of the AI system's behavior throughout its lifecycle.

Python is the dominant language for machine learning model training and inference. A scikit-learn classifier used in hiring decisions, a TensorFlow model in a medical diagnostic tool, a pandas ETL pipeline feeding a credit scoring system — all fall under Article 9's verification obligations. Nagini, applied to the Python data processing and inference code surrounding these models, provides machine-checkable evidence that the code behaves as specified.

Article 15 (Accuracy, Robustness, Cybersecurity) requires AI systems to achieve "appropriate levels of accuracy, robustness, and cybersecurity" throughout their lifecycle. Nagini's postcondition verification ensures that a Python function's output satisfies its specification for all valid inputs — a stronger guarantee than statistical test coverage.

EU AI Act Article 10 — Data Governance

Article 10 requires that high-risk AI systems use training data that is "subject to appropriate data governance and management practices." This includes data completeness, correctness, and the absence of errors and biases. Python ETL pipelines that prepare training data — the pandas, NumPy, and scikit-learn preprocessing code — are directly subject to this obligation.

Nagini can verify properties of data transformation pipelines: that normalization preserves non-negativity, that stratified sampling satisfies proportionality bounds, that null-checking is exhaustive. These are the data governance properties Article 10 implicitly requires.

GDPR Article 25 — Privacy by Design

GDPR Article 25 requires data protection by design: technical measures that ensure that by default only personal data which are necessary for each specific purpose of the processing are processed. Python web backends handling personal data — FastAPI endpoints, Django views, SQLAlchemy ORM operations — are directly subject to this obligation.

Nagini can verify that a Python function processing personal data satisfies its privacy specification: that it returns only the requested fields, that it does not retain data beyond the request scope, that it raises an exception rather than silently returning sensitive data to unauthorized callers. These are the formal properties that "privacy by design" reduces to in code.

Cyber Resilience Act (2027) — Security by Default

The EU Cyber Resilience Act (CRA), applicable from 2027, requires manufacturers of products with digital elements to deliver products that are "secure by default" and to document security properties. For Python web services and API backends, security by default means: input validation is exhaustive, authentication is non-bypassable, sensitive data is never logged.

Nagini's precondition verification can prove input validation properties: that a FastAPI endpoint raises HTTPException for all inputs that violate the API contract, that a Django view never reaches database access code with unsanitized parameters, that a Python function processing JWT tokens raises an exception for all structurally invalid tokens. These are the security properties CRA Article 13 requires in documentation.

The ETH Zurich Programming Methodology Group

Nagini, Prusti, Gobra, and Viper itself all emerge from the Programming Methodology group at ETH Zurich, led by Professor Peter Müller 🇨🇭. The group's research program — dating to the early 2000s — has consistently focused on deductive program verification using permission-based heap models, producing a coherent stack from formal theory to industrial tools.

Key members and contributions:

• Peter Müller 🇨🇭 — group leader, Implicit Dynamic Frames theory, Viper architecture, Prusti co-author
• Marco Eilers 🇩🇪 — Nagini author and primary maintainer (ETH Zurich PhD, now postdoc)
• Alexander Summers 🇨🇭 — Prusti co-author, Viper Silver language design (now University of British Columbia)
• Felix Wolf 🇩🇪 — Gobra co-author (ETH Zurich PhD)
• Malte Schwerhoff 🇩🇪 — Gobra co-author, VerCors collaboration (ETH Zurich, now TU Delft NL)
• Vytautas Astrauskas — Prusti co-author, unsafe Rust verification

The group is funded by the Swiss National Science Foundation (SNSF), by EU Horizon Europe research grants (Switzerland is an associated country for Horizon since 2014), and by ETH Zurich's institutional research budget. All tools are released under open-source licenses (Nagini: MPL 2.0; Prusti: Apache 2.0; Gobra: MPL 2.0).

ETH Zurich is located in Switzerland 🇨🇭 — not an EU member state, but an EU associated country under Horizon Europe, a signatory of the Swiss-EU Framework Agreement, and subject to GDPR for data processing involving EU residents. Swiss federal law (FADP) aligns closely with GDPR. ETH Zurich is outside the US Cloud Act jurisdiction and outside FISA Section 702 — making it a natural partner for EU-sovereign research infrastructure.

Python Versions and Nagini Compatibility

Nagini targets Python 3 and requires MyPy type annotations for field access verification. Fields must be annotated with # type: T comments or PEP 526 variable annotations (field: T) so Nagini can reason about their types statically:

class DataRecord:
    def __init__(self) -> None:
        self.id: int = 0
        self.name: str = ""
        self.value: float = 0.0
        self.active: bool = True

Nagini uses MyPy's type inference infrastructure to resolve types before translation to Viper. This means Nagini inherits MyPy's Python version support — currently Python 3.8 through 3.12. Python 3.12's no-GIL experimental mode (PYTHON_GIL=0) makes Nagini's thread safety verification increasingly relevant as production Python moves toward genuine parallelism.

Comparing Nagini, Prusti, and Gobra

The three Viper front-ends share architecture but differ in specification syntax and target language characteristics:

Nagini predates both Prusti and Gobra by the publication date, establishing that Viper could handle object-oriented dynamically-typed programs before the later tools addressed Rust and Go. The challenge Nagini solved — bringing permission-based heap reasoning to a language without compile-time ownership or borrow checking — required embedding the ownership model entirely in the specification language.

Running Nagini

Nagini is available via pip and requires Java (for Viper backends) and Z3:

# Install Nagini
pip install nagini

# Verify a Python file
nagini verify myprogram.py

# Run with specific Viper backend
nagini verify --backend silicon myprogram.py

For Docker-based deployment on EU infrastructure:

FROM python:3.11-slim

# Java runtime for Viper
RUN apt-get update && apt-get install -y default-jre-headless

# Install Nagini
RUN pip install nagini

WORKDIR /app
COPY requirements.txt .
RUN pip install -r requirements.txt

COPY . .

# Verify before running (CI gate)
RUN nagini verify src/core/validators.py

CMD ["uvicorn", "src.main:app", "--host", "0.0.0.0", "--port", "8000"]

The nagini verify step in the Dockerfile acts as a CI gate: the container build fails if the Python code violates its specifications. This integrates formal verification into the deployment pipeline without requiring developers to run verification locally.

Deploy Nagini on sota.io — EU-Native PaaS

sota.io is the EU-native PaaS for Python and formal verification workloads — GDPR-compliant infrastructure, managed PostgreSQL 17, zero DevOps overhead. Deploy your Nagini-verified Python application directly from git:

# Deploy Python + Nagini to EU
sota deploy --region eu-west

sota.io runs on EU-resident servers under German and Irish data protection jurisdiction. No US Cloud Act exposure. No FISA Section 702. Full GDPR compliance. For teams building EU AI Act-compliant systems, European data residency is not optional — it is the baseline.

Free tier available. No credit card required to start.

Conclusion

Nagini completes the Viper ecosystem's coverage of the three dominant languages of modern software systems:

• Prusti — Rust systems programming: memory safety, embedded systems, OS kernels
• Gobra — Go cloud-native infrastructure: Kubernetes, Docker, Prometheus, service meshes
• Nagini — Python AI/ML and web backends: data pipelines, inference services, regulated APIs

All three share ETH Zurich's Viper infrastructure, Z3 as the SMT solver, and Implicit Dynamic Frames as the heap model. A team building a system with a Go service mesh, Rust cryptographic library, and Python ML inference layer can apply formal verification uniformly across all three using the same conceptual model.

For EU teams deploying under the AI Act, GDPR, or the Cyber Resilience Act, Nagini provides machine-checked evidence that Python code satisfies its behavioral specification — the kind of evidence that Article 9 risk management systems and CRA documentation requirements are increasingly expected to include.

Marco Eilers and Peter Müller developed Nagini at ETH Zurich. The tool is open source under MPL 2.0 and available at github.com/marcoeilers/nagini. The Viper project is at viper.ethz.ch.

See Also

• Deploy Viper to Europe → — Permission-based IVL (ETH Zurich 🇨🇭): Silver IL, Silicon/Carbon backends, the engine Nagini targets
• Deploy Prusti to Europe → — Viper-based Rust verifier (ETH Zurich 🇨🇭): same Viper/Silicon/Z3 backend, IDF permissions for Rust ownership
• Deploy Gobra to Europe → — Viper-based Go verifier (ETH Zurich 🇨🇭): goroutine/channel separation logic, Kubernetes/Docker verification
• Deploy Creusot to Europe → — EU-native Rust verifier (INRIA Saclay 🇫🇷): WhyML/Alt-Ergo, prophecy variables, 100% French EU stack
• Deploy VeriFast to Europe → — Separation logic verifier for C/Java (KU Leuven 🇧🇪): the conceptual predecessor to Viper IDF