Prototype Verification System (PVS)

The PVS interactive theorem prover combines an expressive specification language based on higher-order logic with powerful proof automation and extensive formalized libraries. The specification language supports parametric theories, algebraic and coalgebraic datatypes, dependent tuple, record, function, and array types, dependent predicate subtypes, and constructs for building, using, and updating data represented by these types. The prover integrates satisfiability solvers for Boolean and theory constraints with interactive support for induction, rewriting, case analysis, quantifier reasoning, model checking, and simplification. The PVS libraries span multiple branches of mathematics and computing. Nearly all of the PVS specification language is executable, with support for code generation to Common Lisp and C, and prototype code generators for Rust and oCaml.