Rocq Prover icon
Rocq Prover icon

Rocq Prover

A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.

Rocq's highly expressive type system and proof language enable fully mechanised verification of programs with respect to strong specifications in a wide variety of languages.

Cost / License

  • Free
  • Open Source

Application type

Platforms

  • Mac
  • Windows
  • Linux
The Rocq Prover provides many mechanisms to tailor the environment to one's requirements and structure developments.
The Rocq Prover offers a finely-tuned proof engine and kernel implementation allowing large-scale formalization, with efficient bytecode and native conversion checkers relying on the OCaml runtime.
Rocq Prover alternatives  
-
No reviews
4likes
0comments
4alternatives
0news articles

Features

Suggest and vote on features
  1.  Ad-free

 Tags

  • proof-assistant
  • Math
  • safety
  • formal
  • verification

Rocq Prover News & Activities

Highlights All activities

Recent activities

Show all activities

Rocq Prover information

  • Developed by

    FR flagINRIA

  • Licensing

    Open Source (LGPL-2.1) and Free product.

  • Alternatives

    4 alternatives listed

  • Supported Languages

    • English
    • French

AlternativeTo Categories

Development, Education & Reference

Popular alternatives

View all
Rocq Prover was added to AlternativeTo by greenrd on and this page was last updated .
No comments or reviews, maybe you want to be first?
Post comment/review

What is Rocq Prover?

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Rocq Prover Videos

Official Links

AppStores & Other Links