PVS is a wide-spectrum specification language and theorem prover that has been employed in a number of significant verification projects. The  use of dependent predicate subtypes in PVS ensures that specifications are both mathematically and computationally coherent by eliminating such anomalies as division by zero, real square roots of negative numbers, numeric over ow/under ow, and out-of-bounds array accesses. Almost all of the PVS specification language, which is based on higher-order logic, is executable as an applicative functional language. The PVS type system helps ensure that the generated code is type and memory safety. Type information can also be exploited to optimize the representation of data.

The PVS2C code generator targets the production of efficient, readable, standalone code in a subset of the C programming language from verified PVS definitions. The PVS2C generated code can be easily integrated into existing systems that are based on C or C++. Code generation is useful for validating specifications and building reference implementations.

PVS2C offers numerous benefits for crafting verified code. The generated code is memory-safe, type-safe, and free of exceptions. Programs can be written and optimized at a high level of abstraction to streamline proofs without significantly sacrificing performance. The primary advantage is that specifications, implementations, and proofs can be constructed in a single unified framework. Future work includes the extension of code generation to concurrent execution and the translation validation of the generated code.