Explore projects

Mirror for CI/CD purposes only.

A Kôika implementation of a pipelined RV32I processor with interruptions and exceptions

Utilities for dealing with RISC-V instructions in Coq

Things which probably ought to be in Coq's standard library

An efficient bitvector type for Coq

A rule-based HDL embedded within Coq

GitLab mirror of https://github.com/math-comp/math-comp

Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.

Apps to compile from skel to gallina for use with the Coq Proof Assistant

CoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

A Coq formalization of real analysis compatible with the standard library.

An LR(1) parser generator for OCaml.

implementation and metatheory of time credits and time receipts in Iris / Coq

This repository contains the Coq/Iris proofs that accompany the paper Spy game---Verifying a local generic solver in Iris

CoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.