The best way to install VST 2.13 is through the Coq Platform release for Coq 8.18, coming soon in November/December 2023; or through opam, as coq-vst (64-bit mode) or coq-vst-32 (32-bit mode) from the coq-released archive.

Minor improvements in this release:

• Improved error diagnostics when compspecs mismatch
• Improved error diagnostics when change_compspecs fails
• Improved error diagnostics when VSU has missing (vacuous) funspec
• Int64.repr is Transparent, consistent with Int.repr
• forward tactic is slightly more careful about not simplifying user's terms
• bug fixes and improved diagnostic messages in list_solve tactic
• field_compatible0_Tarray_offset no longer requires naturally_aligned hypothesis
• 'forward' now interacts better with 'localize/unlocalize' (#773)
• Performance improvements in VSU system (#716)
• VSU permits sharing of globals between compilation units (#713)
• Compatible with Coq 8.18.0, 8.17.1, 8.16.1; with CompCert 3.13.1, 3.12, 3.11.

VSTlib

Install VSTlib, a separate package from VST, as coq-vst-lib through the Coq Platform or from the coq-released opam archive.