Coq Platform2025.01.0

Coq Platform lets users write formal specifications and construct proofs that a computer checks, addressing the need for mathematical and software reasoning with precise, machine-verified results. It is a formal proof management system built around the Rocq Prover, an interactive theorem prover and dependently typed programming language for mechanised reasoning.

Its expressive type system and proof language can verify programs against strong specifications and support mathematical developments through the Curry–Howard connection between logic and computation. Applications range from verified software and hardware models to low-level program verification and homotopy type theory, with notable use in projects such as Mathematical Components and the CompCert verified C compiler. Users can tailor developments with scoped notation, coercions, typeclasses, metaprogramming, proof strategies, and embedded domain-specific logics.

The proof engine includes bytecode and native conversion checkers running on the OCaml runtime, while extraction facilities allow verified code to interoperate with programs written in other languages. It suits researchers, educators, and developers working on theorem proving, formal mathematics, programming-language semantics, and high-assurance software or hardware.

Release information for Rocq Platform 2026.07.0 notes that native_compute support was re-enabled with OCaml 5, although architecture-specific code means that support currently covers only some x86 configurations.