Hi everyone, I'm the main author of the tool; it's really cool to see that there's some interest in this :) If you have any questions, I'd be happy to answer them.
We actually named it after the Harry Potter snake :) There was a wiki at some point that stated that Nagini was a hybrid between a Python and a Viper (Viper is the verification framework that we build on), so that's why.
We use the term "memory safety" very broadly; what we meant was the absence of runtime errors (e.g., out-of-bounds list accesses), uncaught exceptions, concurrent modification, basically anything that would lead the program to crash.
Those aren't memory unsafe in the original sense of the word in Python, but they still crash the program.
Additionally, we prove the absence of data races between threads.
