A barely functional, wildly incomplete and basically undocumented Rust crate whose aim is to let you write Games for the Playdate handheld gaming system in Rust.

A wrapper for cargo to use creating games for the Playdate handheld gaming system.

Lean 4 programming language and theorem prover

A Proof-oriented Programming Language

Doom port to Playdate based on Chocolate Doom

Pure DOOM - Single Header Doom Source Port

plasTeX plugin to build formalization blueprints.

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

A collection of tools for writing technical documents that mix Coq code and prose.

Tricks you wish the Coq manual told you [maintainer=@tchajed]

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

Mirror of Software Foundations in PDF

irwin - the protector of lichess from all chess players villainous

An HTML+CSS template for making more accessible posters

Convert Haskell source code to Coq source code.

This repo is the new home of Proof General

Lean Theorem Prover

Code and resources for the paper: "Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs"

A simple raytracer written in Lean 4

Haskell to JavaScript compiler, based on GHC

A LLVM-based static analysis framework.

Haskell Reflex mine sweeper

A simple tar implementation in C

A very simple tar archive processing library

Sail architecture definition language

Proof of Concepts (PE, PDF...)

CakeML: A Verified Implementation of ML

Poly/ML

An educational software system of a tiny self-compiling C compiler, a tiny self-executing RISC-V emulator, and a tiny self-hosting RISC-V hypervisor.

Convert Haskell source code to Coq source code