PV4 Naginiverifies general properties like termination and deadlock freedom of Python programs

Application domain/field

Type of tool

Static verifier/deductive verifier

Expected input

Source code (statically-typed) with specifications (pre-/postconditions/loop invariants/etc.)


Python file

Expected output

Verified (i.e. specification holds) or an error


Automated verifier for statically-typed, concurrent Python 3 programs. The Python program is encoded into a Viper program. The program can then be verified using either symbolic execution or verification condition generation. "Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior." Uses Viper, mypy, Boogie
Concurrency Python


Related papers

Last publication date

18 July 2018

Related tools

Tools that also use Viper as a back end for verification: Gobra, Prusti and VerCors.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.