Come, Nagini. We need to verify that Python code
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.
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:
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.