At a Glance
| Applications | Theorem Prover |
| Developers | Rocq Team |
| Inputs | Rocq |
| Interfaces | CLI |
| Licenses | LGPL-2.1 |
| Maintenance | Actively Maintained |
Description
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
The Rocq Prover was formerly known as the Coq Proof Assistant.