A modern commutative diagram editor for the web.

Toggle Xorg monitors between color and grayscale mode

Datatypes as quotients of polynomial functors

Autoware - the world's leading open-source software project for autonomous driving

incone: information theoretical continuity.

A deep-embedding formalization of modal logic in Coq

T2 Temporal Prover

The Leon system for verification, synthesis, repair

Parameter Synthesis in Markov Models

Rust and C Benchmarks

A formalization of properties of a simple imperative, memory-safe language.

Anvil is an experimental framework to build practical, formally verified, cluster management controllers.

rt-app emulates typical mobile and real-time systems use cases and gives runtime information

A Coq library for parametric coinduction

An emacs tags tool for Verus code.

AlphaVerus: Formally Verified Code Generation through Self-Improving Translation and Treefinement

VAST is an experimental compiler pipeline designed for program analysis of C and C++. It provides a tower of IRs as MLIR dialects to choose the best fit representations for a program analysis or fu…

A Library for Representing Recursive and Impure Programs in Coq

TOPSY - A Teachable Operating System. Swiss Federal Institute of Technology, Computer Engineering and Networks Laboratory

Fil-C: completely compatible memory safety for C and C++

Generic abstract algebra functionality in pure Julia (no C dependencies)

Human-in-the-loop playground for the talk “AI-Optimised Vim Keybindings: HCI-Driven HITL Interfaces”.

🌘 Darktile is an experimental/abandoned GPU rendered terminal emulator designed for tiling window managers.

A curated list of awesome C++ (or C) frameworks, libraries, resources, and shiny things. Inspired by awesome-... stuff.

A list of Free Software network services and web applications which can be hosted on your own servers

Coq library for rose trees

JSON in Coq

Mechanization of AADL in Coq