169 Open source projects that are alternatives of or similar to LibHyps

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

Reference sheet for the Coq language.

Mtac in Agda

Coq to OCaml FFI made easy [maintainer=@lthms]

Formalization of the basic actuarial mathematics using Coq

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

GAPT: General Architecture for Proof Theory

A minimalistic blockchain consensus implemented and verified in Coq

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

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

Goose converts a small subset of Go to Coq

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

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

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

Rainbow Six Siege map quick references

No description or website provided.

Prototipo inicial de un juego tactico. Este proyecto solo alberga unos pocos assets con licencia free y el core de un sistema de combate tactico por turnos.

Generate chess puzzles / tactics from a pgn file

No description or website provided.

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

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

Gallina to Bedrock2 compilation toolkit

The Vellvm (Verified LLVM) coq development.

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

FSCQ is a certified file system written and proven in Coq

Metaprogramming in Coq

hypothesis strategies for generating SQLAlchemy objects

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

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

Tools, documentation and resources for creating front-end pages and apps in Hypothesis

Mutation analysis tool for Coq verification projects

Formalization of Typed Assembly Language (TAL) in Coq

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

A core language for rule-based hardware design 🦑

Jupyter kernel for Coq

Stable sort algorithms and their stability proofs in Coq

A TACtic library for Agda

Idris tactics for (commutative) monoids

An Obsidian.md plugin that syncs highlights from Hypothesis.

Template project for program verification in Coq

Coq plugin embedding elpi

A framework for implementing and certifying impure computations in Coq

Proof of concept to generate safe and fast JavaScript

Generate arbitrary queries matching your GraphQL schema, and use them to verify your backend implementation.

A mechanisation of Wasm in Coq

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

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

A command line utility to generate a knowledge base from Hypothesis annotations

Voevodsky's original development of the univalent foundations of mathematics in Coq

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.

A Learning Environment for Theorem Proving with the Coq proof assistant

Formalization of the polymorphic lambda calculus and its parametricity theorem

Randomized Property-Based Testing Plugin for Coq

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

🐣 A blog engine written and proven in Coq

Archive for all Coq related OPAM packages organized in various repositories

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

Hypothesis and statistical testing in Python

The formal proof of the Odd Order Theorem

Partial Commutative Monoids