Explore projects

An extended "Standard Library" for Coq. [coqdoc]

The Coq development of LambdaRust

Axiomatic pWCET, formalized in Coq

opam repository for development versions of things we develop.

Safety of a syntactically unsafe symbol ADT.

Some example verification demonstrating the use of Iris.

A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.

A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)

This repo contains our prototype implementing the generalised projection of global types from our MST framework with generalised choice.

Maintainer: Felix Stutz

The Coq development for Iris. [project website] [coqdoc]

Instrumented fork of Apache Kafka from GitHub

The main Coq development.

An extended "Standard Library" for Coq. [coqdoc]

Prototype gRPC server with a customizable topology; principally used for Hindsight evaluation.

PCTCP (Probabilistic Concurrency Testing with Chain Partitioning) algorithm for testing Cassandra system. Implemented on top of SAMC/DMCK distributed system model checking tool.

The Coq development for Iris. [project website] [coqdoc]