Displaying 1 to 20 from 89 results

coq - Coq is a formal proof management system

  •    OCaml

Coq is a formal proof management system. 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. Download the pre-built packages of the latest release for Windows and MacOS; read the help page on how to install Coq with OPAM; or refer to the INSTALL file for the procedure to install from source.

awesome-software-quality - List of free software testing and verification resources


This page collects resources for anyone considering the use of software testing and formal methods. There are many axes along which one can organize such a list, such as the level of expertise of the intended audience (from experts to the public at large) or disciplinary orientation (computer science, mathematics, mathematical logic, etc.). Here I have chosen to classify the material by type of subject matter.

CompCert - The CompCert formally-verified C compiler

  •    Coq

The verified C compiler. The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors.

verdi - A framework for formally verifying distributed systems implementations in Coq

  •    Coq

A framework for formally verifying distributed systems implementations in Coq.We recommend installing Verdi via OPAM, which will automatically build and install its dependencies.

Cosette - Cosette is an automated SQL solver powered by Coq/Lean and Rosette.

  •    Lean

Cosette is a language, and an automated solver for reasoning SQL equivalences.

UniMath - This coq library aims to formalize a substantial body of mathematics using the univalent point of view

  •    Coq

This Coq library aims to formalize a substantial body of mathematics using the univalent point of view. See INSTALL.md.

Coq Au Win


Integration of Coq and the gallina language into Visual Studio 2010.

category-theory - A formalization of category theory in Coq for personal study and practical work

  •    Coq

This development encodes category theory in Coq, with the primary aim being to allow representation and manipulation of categorical terms, as well realization of those terms in various target categories. Core Theory, covering topics such as categories, functors, natural transformations, adjunctions, kan extensions, etc.

StructTact - Coq utility and tactic library.

  •    Coq

StructTact is a Coq library of "structural tactics" (StructTactics.v) as well as libraries containing lemmas about lists (Util.v), finite types (Fin.v), and orders on strings (StringOrders.v) that use the tactics library.These files were originally developed in the context of Verdi, but have since been factored out to make them easier to use in other projects.

verdi-raft - An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

  •    Coq

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.Then, run ./configure in the Verdi Raft root directory. This will check for the appropriate version of Coq and ensure all necessary Coq dependencies can be located. By default, Verdi, StructTact, and Cheerios are assumed to be installed in Coq's user-contrib directory, but this can be overridden by setting the Verdi_PATH, StructTact_PATH, and Cheerios_PATH environment variables.

dsss17 - A Nix project for building all the dependencies needed at DeepSpec Summer School 2017

  •    Nix

To build all the dependencies needed for the DeepSpec Summer School 2017, you will need to execute the following from a recursive clone of this repository. This ensures any work you do in the /home/nix/work directory in the container (the default starting location), is saved in the ./work directory where you started the container.

pnp - Lecture notes for a short course on proving/programming in Coq via SSReflect.

  •    Coq

"Programs and Proofs: Mechanizing Mathematics with Dependent Types". Just run make. This will compile all lecture files, solutions and create the file latex/pnp.pdf with lecture notes.

coq-ext-lib - A library of Coq definitions, theorems, and tactics.

  •    Coq

A collection of theories and plugins that may be useful in other Coq developments.

parseque - Total Parser Combinators in Coq

  •    Coq

This is a port of agdarsec to Coq.

ceps - Coq Enhancement Proposals


This repository contains the Coq Enhancement Proposals (CEP), the Coq equivalent of RFCs, PEPs and the like.

opam-coq-archive - Archive for all Coq related OPAM packages organized in various repositories

  •    Javascript

All OPAM repositories for Coq packages live here. Packages are organized according to the layout. We follow the model of the Coq website. One should invoke make COQWEB=path/to/coq/www to generate the web pages using the same header, footer and yamlpp used by the Coq website (it is expected to be in path/to/coq/www/yamlpp-0.3/yamlpp. The destination folder is www/.

proofs - A selection of formal developments in Coq.

  •    Coq

A selection of formal developments in Coq. Make sure you have the dependencies listed below. Then you can run make to verify the proofs. You can also use make lint to invoke the linters. The build artifacts can be removed with make clean.

cheerios - Formally verified Coq serialization library with support for extraction to OCaml

  •    Coq

Cheerios is a formally verified serialization library for Coq. It defines a typeclass for serializable types and defines instances for many built-in types. The specification of a serializable type requires that serializing followed by deserializing is the identity. By linking extracted code with the Cheerios OCaml runtime support library, verified serializable types can be used in executable programs.

We have large collection of open source products. Follow the tags from Tag Cloud >>

Open source products are scattered around the web. Please provide information about the open source projects you own / you use. Add Projects.