Skip to content
| Marketplace
Sign in
Visual Studio Code>Other>ProVerif LanguageNew to Visual Studio Code? Get it now.
ProVerif Language

ProVerif Language

ProVerif

|
784 installs
| (0) | Free
Language support for ProVerif
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

VSCode ProVerif Language Service

Available on the Visual Studio marketplace Available on the Open VSX marketplace

Visual Studio Code extension for ProVerif files (.pv, .pvl, .pcv).

Screenshot showing how the extension shows errors from ProVerif

Functionality:

  • Adds semantic syntax highlighting.
  • Highlights the first syntax error. For libraries, see below.
  • Hover over an identifier to learn more about it.
  • Press CTRL and click on an identifier to navigate to its definition or find all references of the definition.
  • Press F2 to rename an identifier.
  • Press CTRL+SHIFT+Space to show signature help (automatically shown when typing ().
  • Press CTRL+SHIFT+B to execute ProVerif over the currently opened file.

Settings:

  • Proverif Path: Custom path to the proverif binary (else taken from $PATH).
  • Parent Folder Discovery Limit: Parent folders to read until discovery stops (e.g. to find references).

You might want to further customize how the extension affects VSCode, see CUSTOMIZATION.md.

Libraries (.pvl)

If your .pv or .pvl file depends on libraries, include a corresponding comment (* -lib {library_path}.pvl *):

(* -lib types.pvl *)

fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.

Logs (.pv.log)

Store output of ProVerif in .pv.log files, for some basic syntax highlighting, and process reference navigation (press CTRL and click on e.g. {21} to navigate to its definition).

  • Contact us
  • Jobs
  • Privacy
  • Manage cookies
  • Terms of use
  • Trademarks
© 2025 Microsoft