Thesis/Dissertation Template for graduate students at Augusta University

Dafny is a verification-aware programming language

The Ott tool for writing definitions of programming languages and calculi

SeaHorn Verification Framework

A friendly programming language from the future

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.

an educational compiler intermediate representation

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

A textbook on informal homotopy type theory

The Termination Problem Database

A Coq IDE build on top of Proof General's Coq mode

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

Mathematical Components

Template for Augusta University Letterhead

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

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

Easy to maintain open source documentation websites.

The Penn Locally Nameless Metatheory Library

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

CoFloCo is a static analysis tool written in prolog to infer automatically symbolic complexity bounds of imperative and recursive programs.

An introduction to programming language theory in Agda

LaTeX Examples Document Source

Scrapers for extracting articles from major Finnish journalistic media outlets

Official repository for Citation Style Language (CSL) citation styles.

Formal Reasoning About Programs

a list of 100+ awesome open source android apps 📱

A modern load testing tool, using Go and JavaScript

Csmith, a random generator of C programs

The CompCert formally-verified C compiler