marcoeilers
commented
2 months ago We're not planning to support interactive theorem provers like Coq in any direct way. Nagini targets Viper as a backend, which currently relies exclusively on SMT solvers. In principle, it would probably be possible to generate proof obligations for interactive theorem provers instead. However, since Nagini is designed to target SMT-based Viper, that would almost certainly result in both a huge number of simple proof obligations (that SMT solvers can prove automatically but that would be a problem in a more interactive setting) and some more complex proof obligations, the ones that cause performance issues and that would be a good target for interactive provers, that are not expressed in a way that is optimal for interactive proofs.
I'm aware that Nagini's verification performance can get bad pretty quickly for Python code or specifications following certain patterns. However, in many cases, this can be mitigated by using the right Nagini or Viper options. For the most part, that's not well-documented anywhere, but feel free to file issues and I'll try to help.
Additionally, we are aiming to make Nagini more efficient in a couple of ways: a) there are several known inefficiencies in Nagini's encoding from Python to Viper that we are aiming to eliminate in the next couple of months b) we keep improving performance (and performance tuning options) in Viper itself c) Viper is likely to get some experimental features that will enable more interactive proofs in the near future (not on the level of Coq or similar tools; the goal is to allow users to perform some interactive proofs steps before the SMT solver is used). If this turns out to be a useful feature, we might try to integrate these features in Nagini.
Magikaaarp
Hello Nagini Team,
I hope this message finds you well. I am currently considering using Nagini for formal verification of a complex Python third-party library. I watched the YouTube recording of your talk on SPS23 and worried about the efficiency and other limitation you've mentioned. So I wondered if I could replace SMT solvers with proof assistants like Coq.
It would be beneficial to have an interface that allows users to generate proof-goals that cannot be automatically solved by Z3. This would enable seamless integration with formal proof assistants, allowing for deeper verification and reasoning about code correctness. By providing this interface, Nagini can enhance its usability for users seeking high reliability and complexity in software development.
I would appreciate any insights into whether this functionality is planned for future releases or if there are alternative approaches to achieve similar results. Thank you for considering this request. I look forward to your response!
Best regards, Magi