VSCode-PVS is a modern integrated development environment for the
Prototype Verification
System (PVS). This new environment integrates
the editing and proof management functionalities of PVS in Visual
Studio Code, a popular code editor widely used by software
developers. VSCode-PVS provides functionalities that developers expect
to find in modern verification tools, but are not available in the
standard Emacs front-end of PVS, such as auto-completion,
point-and-click navigation of definitions, live diagnostics for
errors, and literate programming.
VSCode-PVS is publicly available under NASA's Open Source Agreement from GitHub.