Archive of Formal Proofs The Top 100 Theorems in Isabelle Formalizing 100 Theorems Library of Formalized Mathematics for Isabelle/Isar UTP(Unifying Theories of Programming) in Isabelle Isabelle/DOF:Document Ontology Framework on top of Isabelle Isabelle/Spartan:A minimal intensional dependent type theory object logic for Isabelle Isabelle/HOL-OCL:an interactive proof environment for the Object Constraint Language (OCL) HOL-TestGen:a is a test case generator for specification based unit testing seL4 verification Verified Software Toolchain lets-prove-leftpad Type Theory for All