Top 153 coq open source projects

Homotopy type theory

Implementation of sprintf for Coq

Verified vector clocks, with Coq!

A Hello World program in Coq.

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

Coq executable semantics and resource verifier

Formalisation of the linear lambda calculus in Coq

Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.

Coq code accompanying several articles on semantics of functional programming languages

Combinatorial species in HoTT

An introductory tutorial for the Coq proof assistant.

CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)

Formalization of C++ for verification purposes.

Automation for de Bruijn syntax and substitution in Coq

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

A Coq library for extensional finite sets and comprehension

Certified Relational to Imperative

Coq proofs of exercises in Pierce's book

KCoFI Pudding: The formal proofs for the KCoFI system

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

An axiom-free formalization of category theory in Coq for personal study and practical work

《软件基础》中译版 Software Foundations Chinese Translation

Cosette is an automated SQL solver.

A framework for formally verifying distributed systems implementations in Coq

Formal Reasoning About Programs

A port of Coq to Javascript -- Run Coq in your Browser

This repo is the new home of Proof General

Cryptographic Primitive Code Generation by Fiat

Mathematical Components

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.

Tricks you wish the Coq manual told you

A Coq IDE build on top of Proof General's Coq mode

An introductory course to Homotopy Type Theory

Convert Haskell source code to Coq source code

A gently curated list of companies using verification formal methods in industry

Verified Software Toolchain

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

IO for Gallina

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

A proof of Abel-Ruffini theorem.

Formal verification of OCaml programs

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Finite sets, finite maps, multisets and generic sets

Ltac2 tutorial

Mtac in Agda

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Multinomials for the Mathematical Components library.

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

A Coq library providing tactics to deal with hypothesis

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

A framework for implementing and certifying impure computations in Coq

Jupyter kernel for Coq

No description or website provided.

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

The formal proof of the Odd Order Theorem

Mutation analysis tool for Coq verification projects