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

Verifying concurrent crash-safe systems

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.

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

Ring, field, lra, nra, and psatz tactics for Mathematical Components

Micromega tactics for Mathematical Components

Stable sort algorithms and their stability proofs in Rocq

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

A framework for Systems Verification of categories, Theories and Meta Theories in Lean, Rocq, C# and F#.

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).

My current starting point for projects using Rocq.