152 Open source projects that are alternatives of or similar to Software Foundations

Mutation analysis tool for Coq verification projects

Template project for program verification in Coq

A proof of Abel-Ruffini theorem.

Jupyter kernel for Coq

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

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

Partial Commutative Monoids

Mathematical Components

Formalization of the polymorphic lambda calculus and its parametricity theorem

Ltac2 tutorial

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

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

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

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.

This repo is the new home of Proof General

Gallina to Bedrock2 compilation toolkit

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

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

Cosette is an automated SQL solver.

Intermediate Memory Model (IMM) and compilation correctness proofs for it

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

Archive for all Coq related OPAM packages organized in various repositories

Tricks you wish the Coq manual told you

Formalization of the basic actuarial mathematics using Coq

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

A Coq library providing tactics to deal with hypothesis

A core language for rule-based hardware design 🦑

Convert Haskell source code to Coq source code

A framework for implementing and certifying impure computations in Coq

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

No description or website provided.

Verified Software Toolchain

The formal proof of the Odd Order Theorem

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

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

IO for Gallina

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

Cryptographic Primitive Code Generation by Fiat

A formally verified high-level synthesis tool based on CompCert and written in Coq.

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

A library of mechanised undecidability proofs in the Coq proof assistant.

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

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Formal verification of OCaml programs

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

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.

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Finite sets, finite maps, multisets and generic sets

Convert Haskell source code to Coq source code.

A framework for formally verifying distributed systems implementations in Coq

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Mtac in Agda

Formalization of Typed Assembly Language (TAL) in Coq

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

Multinomials for the Mathematical Components library.

KCoFI Pudding: The formal proofs for the KCoFI system

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

Formal Reasoning About Programs

An introductory course to Homotopy Type Theory

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