rocq

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

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Visual Studio Code extension for Coq

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.

A Rocq version of the miniF2F dataset

BigRocq is a utility, that takes a Rocq (former Coq) project as input and uses domain knowladge to increase a number of theorems in the dataset by a significant factor.

Local computation rules in type theory

Notes and Learning Material for the course "Proofs, Programs and Types" taught at IIT Palakkad

Proof checker from scratch in Python and coq / rocq

A tutorial on well-founded recursion in Rocq

Prove spec for a program that increases a list and sums it in parallel (Final project, CS 472, Spring 2024 @ UIC).