VSTlib release 2.15.1

VSTlib 2.15.1 is compatible with VCFloat 2.3.

VST version 3.1beta

VST version 3.1beta (VST on Iris), compatible with Coq 8.19-8.20, CompCert 3.15, and Iris 4.3.0.

VST version 2.15 and VSTlib version 2.15

For Coq 8.19-8.20 and CompCert 3.15

VST version 3.0beta2

The first full beta release of VST 3.0, VST on Iris. Compatible with Coq 8.18-8.19 and CompCert 3.13.1. Based on Iris 4.2.0, which can be installed via OPAM (as coq-iris.4.2.0).

VST version 3.0beta1

The first beta release of VST 3.0, VST on Iris. Compatible with Coq 8.17-8.19 and CompCert 3.13.1. Based on coq-iris.dev.2024-02-04.0.0771fa71, which can be installed via OPAM:

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-iris.dev.2024-02-04.0.0771fa71

VST version 2.14

VST version 2.14, compatible with Coq 8.17-8.19 and CompCert 3.13.1

VST version 2.13 and VSTlib version 2.13

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.

VSTlib release 2.12

VSTlib: VST-verified C library for VST-verified clients

These program modules, in the form of Verified Software Units, may be linked with client-module code (at the .c/.o level) and proofs (at the .v level). This release of VSTlib is expected to be compatible with VST 2.11.1 and VST 2.12.

VST version 2.12

The best way to install VST 2.12 is through the Coq Platform release 2023.03, or more recent.

New in this release:

• entailer!! tactic that does not put so many propositions above the line, compared to entailer!. See the end of the entailer! chapter in the manual.
• VSTlib, a new library of Verified Software Units; currently has interface to malloc/free library, math library, threads and locks libraries.
• Compatible with Coq 8.16 and 8.17, and with CompCert 3.12.

VST version 2.11.1

The best way to install VST 2.11.1 is through the Coq Platform release 2022.09.1.