The Vellvm (Verified LLVM) coq development.

org-mode modules for citations, cross-references, bibliographies in org-mode and useful bibtex tools to go with it.

Moloch is a minimalist, feature-rich Beamer theme for LaTeX presentations with a clean design and extensive customization options.

🍃 SimplePlus - A minimalist and clean LaTeX Beamer theme

A modern LaTeX Beamer theme

Simple, typographic beamer theme

A Rust verification tool

A foundational framework for modular cryptographic proofs in Coq

Shrinking induction-recursion... sometimes you just wanna be small!

coinduction library for Coq

An extremely fast Python package and project manager, written in Rust.

A formal development of constructive domain theory in Coq

Malloc / Free / Realloc / Calloc implementation using a red-black tree

Gallina to Bedrock2 compilation toolkit

Bump allocator in C

Reimplementing malloc(), calloc(), realloc(), free() in c from scratch using system calls

Language for high-assurance and high-speed cryptography

Named overlays for Beamer

Mechanized baselines for various type system features

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

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source

A radical OCaml build system

The Lean Computer Science Library (CSLib)

Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]

Stdlib for the Rocq Prover

Slides and sources for talks on Tree Borrows

A small (2Kb zipped minified) tree-shakeable functional library to manipulate generic rose (a.k.a multi-way) trees