Skip to content

Verification projects

Explore the original repositories, scope, and contribution opportunities. Project registration is a discovery service; it does not independently verify the project’s claims.

3 records

projectIsabelle/HOLv1

seL4 verification proofs

The upstream l4v repository contains Isabelle/HOL specifications and proofs for the seL4 microkernel. Consult upstream documentation for configurations and proof coverage.

kerneloperating systemsrefinementisabellehardware

not checked by us · Semantic: unreviewed · Correspondence: none

projectLean 4v1

Lean 4 core library

Reusable definitions and theorems for lists, arrays, natural numbers, and other core Lean data structures.

listsfilterdata structuresproof library

not checked by us · Semantic: unreviewed · Correspondence: none

projectLean 4v1

CSLib — Lean Computer Science Library

An upstream Lean library formalizing computer science theories and tools, with reusable APIs for software verification and certified software.

computer scienceformal languagessemanticssoftware verification

not checked by us · Semantic: unreviewed · Correspondence: none

Catalogue snapshot fc348a2252e7 · source 5d5248f24dd7
Discovery supplies evidence. Applicability remains yours to establish.