Python API for lightweight communication with the Rocq proof assistant

Library for structural temporal logic proofs over coinductive, free monads with effects and choice.

Astrological CPU Scheduler

Visual Studio Code extension for Coq

Minimal implementations for dependent type checking and elaboration

Prove functional correctness of Ethereum smart contracts in higher-order logic

Development of an ml compiler to arduino

A readline wrapper

bare metal ARM examples to be run with qemu-system-arm

Language tools for manipulating OCaml programs in Haskell (parser, pretty-printer, ...)

Course Material for "Programming Languages II"

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Verifying the Rust standard library

A gently curated list of companies using verification formal methods in industry

A listing of compiler, language and runtime teams for people looking for jobs in this area

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

Implementations of Fibonacci

The Vellvm (Verified LLVM) coq development.

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

project to automate the modeling of a smart contract as a game

LLMs as Copilots for Theorem Proving in Lean

weird erc20 tokens

Smart contract specification language

emacs major mode for .act specs

🕵️ Haskell STatic ANalyser

The efficient SMT-based context-bounded model checker (ESBMC)

A dead simple Go library for sending notifications to various messaging services.

Symbolic and concrete EVM execution engine