The main Coq development.

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

The Coq development for Iris

The main Coq development of the Prosa project: http://prosa.mpi-sws.org

The Coq development of LambdaRust

Some example verification demonstrating the use of Iris.

This project contains some scripts and other files that are used by many Iris project for their CI

opam repository for development versions of things we develop.

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

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

The Coq development for Iris

An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode

An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode

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

The Coq development of LambdaRust

Code and documents for "Resilient Abstraction-Based Controller Design"

Some example verification demonstrating the use of Iris.

Operational Repaired C11