This webpage showcases several interesting examples that demonstrate features of Nagini, a static verifier for Python 3.

Binary Search Tree

Binary search tree implementation from

Cell and Recell

Demonstration of predicate families; running example of paper 'Separation Logic and Abstraction', POPL 2005.


Method finding a divisor of an integer; demonstrates for loops and break statements.

Hello World (IO)

Program outputting the string 'Hello World', demonstrating input/output verification.


Quicksort implementation from, demonstrating verification of termination.


Different kinds of students enrolling in courses; demonstrating predicate families.

Sum of odd numbers

Calculates the sum of all odd integers in a list; demonstrates pure functions, built-in list types, and continue statements.


Running example from CAV 2018 paper, showing dynamic field addition, quantifiers, predicates and termination verification.


Watchdog continually checks that other threads preserve an invariant on shared data; demonstrates verification of threads, locking, and deadlock freedom.

Empty Example (try your own!)

Input and verify a new example of your own