Nagini
Nagini is an automated, modular verifier for (concurrent) Python programs, based on the Viper verification infrastructure. It supports a rich subset of statically-typed Python 3 as defined in external page PEP 484. Nagini is intended to be able to prove complex properties of real-world user code; in addition to basic safety and functional correctness, its specification language allows specifying properties like input/output behavior, progress properties, and secure information flow. A description of Nagini's specifications can be found external page here.
Nagini was originally developed as part of the VerifiedSCION project; it is open source and available on external page Github.
The easiest way to try it out yourself is to install it from external page PyPI or use the external page Nagini VSCode extension.
Nagini has also served as the basis of 2vyper, a verifier for Ethereum smart contracts written in the Python-like Vyper language.
Project Members
Marco Eilers
Nicolas Ray Klose
Peter Müller
Links
external page Nagini on GitHub
external page Nagini on PyPI
external page Nagini VSCode extension
external page Nagini Wiki explaining its specification language
Publications
- E. Birling and M. Eilers, Towards Cross-Language Verification between Python and C
In International Symposium on Leverating Applications of Formal Methods, Verification, and Validation (ISoLA), 2026. To appear. [PDF] - M. Greutmann and M. Eilers and P. Müller, Modular Reasoning about Object Relations
In Computer Aided Verification (CAV), 2026. To appear. [PDF] - M. Eilers and S. Meier and P. Müller, Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
In Computer Aided Verification (CAV), 2021. [PDF]
- M. Eilers and P. Müller, Nagini: A Static Verifier for Python
In Computer Aided Verification (CAV), 2018. [PDF]
- M. Hassan and C. Urban and M. Eilers and P. Müller, MaxSMT-based Type Inference for Python 3
In Computer Aided Verification (CAV), 2018. [PDF]
Ongoing Student Projects
- Felix Beckers, Practical Work
VS Code Integration for an Automated Python Verifier
Completed Student Projects
- Marco Principe, Bachelor's Thesis
Enabling Ghost Code in the Nagini Verifier - Luca Schafroth, Master's Thesis
Formally Verified ASN.1 Python Encoders and Decoders - Etienne Birling, Master's Thesis
Cross-Language Verification of Python Modules Written in C - Micha Greutmann, Bachelor's Thesis
Enabling Object Equality Reasoning for Python - Pascal Devenoge, Bachelor's Thesis
Specification of Python Math and Data Science Libraries
- Edgars Vitolins, Master's Thesis
Download Verification of Python Code with a Dynamic Object Model (PDF, 549 KB)
- Severin Meier, Master's Thesis
Verification of Information Flow Security for Python Programs - Benjamin Schmid, Bachelor's Thesis
Abstract Read Permission Support for an Automatic Python Verifier - Benjamin Weber, Master's Thesis
Automatic Verification of Closures and Lambda-Functions in Python - Mostafa Hassan, Bachelor's Thesis
Static Type Inference for Python
- Vytautas Astrauskas, Master's Thesis
Input/Output Verification in Viper