Nagini IDE

This VS Code extension provides interactive IDE features for verifying Python programs with the Nagini verifier.

Requirements

The requirements for the Nagini verifier can be found here: https://github.com/marcoeilers/nagini.

Note that the installation command uses pip to install the Nagini verifier.

Features

Commands

This extension provides the following commands:

• Nagini: Select Environment: select a Python environment
• Nagini: Install Nagini: install Nagini from source
• Nagini: Toggle Mode: switch between Server mode (a persistent Nagini server) and Direct mode (a separate Nagini process per verification)
• Nagini: Select Backend: select the backend verifier
• Nagini: Start Verification: start a new verification process
• Nagini: Verify Function at Cursor: verify only the function or method at the cursor position
• Nagini: Stop Verification: stop the current verification process

Settings

This extension provides the following settings:

• nagini.paths.boogieExecutable: specify the path of the Boogie executable used by Carbon
• nagini.verification.timeout: specify the time limit for a verification process
• nagini.verification.additionalArguments: specify additional command-line arguments passed to Nagini during verification (each list item is one argument)

Troubleshooting

Orphaned server process

Occasionally, Nagini's server process may continue running after the extension is deactivated or VS Code is closed. If this happens, it needs to be terminated manually.