Explore projects

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

SimBricks repository mirror, only used for CI. Use https://github.com/simbricks/simbricks

This is the repository for the EU EIC project called SymAware.

opam repository for development versions of things we develop.

Automation for Iris

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

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

Axiomatic pWCET, formalized in Coq

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

Iris with transfinite step-indexing

The Coq development of LambdaRust

Some example verification demonstrating the use of Iris.

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

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)