Explore projects

The Iron logic for precise reasoning about resources [project website]

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

The Coq development of LambdaRust

opam repository for development versions of things we develop.

Some example verification demonstrating the use of Iris.

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

The Coq development for Iris

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

https://os.mpi-sws.org/

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

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