  The steep learning curve of formal technologies is a well-known barrier to
the adoption of formal verification tools in industry. This paper presents
VSCode-PVS, 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. The main features and architecture of the environment are
presented, along with a comparison with other similar tools.
