isabelle-hol

A curated set of links to formal methods involving provable code.

Cogent Project

Verification infrastructure for the Isabelle/HOL interactive proof assistant

Readings on computational logic, interactive theorem proving and functional programming.

Proof exercises in Lean4 and Isabelle/HOL

some sorting algorithms' formalisation

Kategorischer Imperativ in Isabelle/HOL (experimental)

Solutions to the exercises in "Programming and Proving in Isabelle/HOL"

Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).

This educational project was taught at the Deutsche SchülerAkademie in 2024 to a group of 16 talented German high-school student. A report is going to appear in the proceedings of the ThEdu 2026 workshop.

Hello World in Isabelle, compiled to Haskell

A Generic, Executable, and Machine-Checked Framework for Interprocedural Abstract Interpretation in Isabelle/HOL

Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"

Curso de "Razonamiento automático"

「情報数学講座（第7巻）プログラム意味論」（著: 横内寛文）の形式的証明

Source tooling for Isabelle/Isar projects: a formatter, project and source checks, and statistics.

Propositional logic and FOL proofs (froward style)

Advent of Code solutions, in OCaml and (sometimes) Isabelle/HOL