No need to slay this one

Come, Nagini. We need to verify that Python code

© Shutterstock /

Nagini, except for being the… massive friend of he-who-must-not-be-named, is also a static verifier for Python, built on the Viper verification infrastructure. Is it me or did a lot of snakes just started hanging around?

The Harry Potter series might have concluded but, unlike what happened in the popular movies, Nagini gets to live on to tell the tale!

Created by Marco Eilers and Peter Müller,  Nagini is an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure that combines established concepts with new ideas, creating a… slithering verification workflow!

Wizardly skills and specifications

There are a couple of requirements and specifications you need to be aware of if you are interested in becoming Nagini’s next master.

Python Subset: Nagini requires input programs to comply to the static, nominal type system defined in PEP 484 as implemented in the Mypy type checker, which requires type annotations for function parameters and return types, but can normally infer types of local variables.

SEE ALSO: Vibora: A venomous Python client/server framework

Specification Language: Nagini includes a library of specification functions similar to .NET Code Contracts to express pre- and postconditions, loop invariants, and other assertions.

Verified properties: Nagini verifies some safety properties by default: Verified programs will not raise runtime errors or undeclared exceptions.

So, how does it work?

Nagini is based on many techniques used in existing tools like VeriFast, .NET Code Contracts, Viper and more. But it does have a set of new ideas used to verify advanced properties and handle the dynamic aspects of Python. To name a few:

  • Implements a  comprehensive system for verifying finite blocking and input/output behavior
  • Builds on Mypy to verify safety while also supporting important dynamic language features
  • Verifies substantial, real-world code, and is currently used to verify the Python implementation of the SCION internet architecture
  • It is the first tool to enable automatic verification of Python code
  • Multi-domain application:  In addition to memory safety, programmers can choose to prove that a server implementation will stay responsive, that data science code has desired functional properties, or that algorithms terminate and preserve certain invariants

SEE ALSO: Top 5 IDEs and code editors for Python

Nagini’s… slithering verification workflow is depicted below:

Getting started

If you are interested in having a first contact with Nagini, you can try the online version here. Beware, though; this version is rather slow.

Alternatively, if you feel ready to take Nagini for a slide, you can install the plugin via the PyCharm IDE, use it on Ubuntu Linux or Windows.

You can find the CAV 2018 tool paper describing Nagini here and the documentation of Nagini’s specification language here.

Eirini-Eleni Papadopoulou
Eirini-Eleni Papadopoulou was the editor for Coming from an academic background in East Asian Studies, she decided that it was time to go back to her high-school hobby that was computer science and she dived into the development world. Other hobbies include esports and League of Legends, although she never managed to escape elo hell (yet), and she is a guest writer/analyst for competitive LoL at TGH.

Inline Feedbacks
View all comments