20
I Use This!
Very High Activity
Analyzed about 23 hours ago. based on code collected 1 day ago.

Project Summary

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:

* to define functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a relatively small certification "kernel".

Tags

coq extraction functional functional_language language logic mathematics programming proof-assistant proof_assistant proving theorem theoremprover

In a Nutshell, Coq proof assistant...

MIT
Permitted

Commercial Use

Modify

Distribute

Place Warranty

Use Patent Claims

Forbidden

Sub-License

Hold Liable

Required

Distribute Original

Disclose Source

Include Copyright

State Changes

Include License

Include Install Instructions

These details are provided for information only. No information here is legal advice and should not be used as such.

This Project has No vulnerabilities Reported Against it

Did You Know...

  • ...
    65% of companies leverage OSS to speed application development in 2016
  • ...
    search using multiple tags to find exactly what you need
  • ...
    in 2016, 47% of companies did not have formal process in place to track OS code
  • ...
    by exploring contributors within projects, you can view details on every commit they have made to that project

Languages

OCaml
69%
coq
25%
15 Other
6%

30 Day Summary

Jul 25 2025 — Aug 24 2025

12 Month Summary

Aug 24 2024 — Aug 24 2025
  • 2546 Commits
    Down -124 (4%) from previous 12 months
  • 63 Contributors
    Down -1 (1%) from previous 12 months

Ratings

8 users rate this project:
4.875
   
4.9/5.0
Click to add your rating
  
Review this Project!