The Archive of Formal Proofs is a collection of proof libraries, examples,
and larger scientific developments, mechanically checked in the theorem prover
Isabelle. It is organized in the way
of a scientific journal. Submissions are
The archive repository is hosted on Heptapod to
provide easy free access to archive entries. The entries are
tested and maintained continuously against the current stable release of
Isabelle. Older versions of archive entries will remain available.
The editors of the archive are
We aim to strengthen the community and to foster the development of formal
We hope that the archive will provide
- a resource of knowledge, examples, and libraries for users,
- a large and relevant test bed of theories for Isabelle developers, and
- a central, citable place for authors to publish their theories
We encourage authors of publications that contain Isabelle developments
to make their theories available in the Archive of Formal Proofs and to refer
to the archive entry in their publication. It makes it easier for referees to
check the validity of theorems (all entries in the archive are
mechanically checked), it makes it easier for readers of the publication to
understand details of your development, and it makes it easier to use and
build on your work.
All entries in the Archive of Formal Proofs are licensed under
a BSD-style License or
the GNU LGPL.
This means they are free to download, free to use, free to change, and
free to redistribute with minimal restrictions.
The authors retain their full copyright on their original work,
including their right to make the development available under another,
additional license in the future.