Nubo is a repository of interoperable formal proofs.
The goal of Nubo is to make software verification easier by bridging the gaps introduced by the diversity of proof assistants and the lack of standards in the domain of formal proofs.
The Nubo repository is made of formal proofs written in the λΠ calculus modulo. These proofs are easy to check and enable computer scientists and mathematicians to exchange proofs between formalisms.
Nubo already contains proofs from the following systems,
The proofs are available here as tar-gzipped archives. The format of the archives as well as a makefile interface are provided by the nubo repository. It also provides instructions on how to contribute to nubo.