Nagini: A Static Verifier for Python [pdf]

This is really, really cool. It&#x27;s on github at <a href="https:&#x2F;&#x2F;github.com&#x2F;marcoeilers&#x2F;nagini" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;marcoeilers&#x2F;nagini</a> and you can see examples of the syntax here: <a href="http:&#x2F;&#x2F;viper.ethz.ch&#x2F;nagini-examples&#x2F;" rel="nofollow">http:&#x2F;&#x2F;viper.ethz.ch&#x2F;nagini-examples&#x2F;</a><p>In the same way that Python&#x27;s (and Flow&#x2F;Typescript&#x27;s) typing lets you describe argument and return types with no more effort&#x2F;characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there&#x27;s a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It&#x27;s the type of thing that there&#x27;s no reason <i>not</i> to use.<p>It&#x27;s powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: <a href="http:&#x2F;&#x2F;people.inf.ethz.ch&#x2F;summersa&#x2F;wiki&#x2F;lib&#x2F;exe&#x2F;fetch.php?media=papers:viper-vmcai16.pdf" rel="nofollow">http:&#x2F;&#x2F;people.inf.ethz.ch&#x2F;summersa&#x2F;wiki&#x2F;lib&#x2F;exe&#x2F;fetch.php?me...</a> . Very smart stuff around tracking read&#x2F;write dependencies on variables in a programmer-friendly way.

Classic, and nicely done.<p>They did something right that&#x27;s rarely done - their verification extensions to Python are Pythonic. They don&#x27;t use a separate language for invariants and assertions, and they don&#x27;t put the assertions in comments. The assertions are thus part of the program.

Abstract copied from the PDF: We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input&#x2F;output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.

Fun fact:<p>The name, Nagini, derives from the Sanskrit word for &quot;a deity or class of entity or being taking the form of a very great snake, specifically the king cobra, found in the Indian religions of Hinduism, Buddhism and Jainism.&quot;<p><a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;N%C4%81ga" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;N%C4%81ga</a>

I’m going to get blasted on this but what if all this python static type checking and such is not needed. Python is python. It’s slower than other languages and that’s ok. I fear that too much is being done and slowly the clean syntax of the language is being eroded.

Hi everyone, I&#x27;m the main author of the tool; it&#x27;s really cool to see that there&#x27;s some interest in this :) If you have any questions, I&#x27;d be happy to answer them.