hol4

A verification toolchain for Rust programs

Binary analysis in HOL

P4 formalization using Ott and HOL4

Interactive Theorem Proving course using HOL4

Certified proof checker for Fitch-style propositional logic proofs

Formal definition, metatheory, and tools for the Machine Independent Language using HOL4 and CakeML

Ready-to-run copy of Milawa on Jitawa

Dockerfiles to build HOL4 (https://github.com/HOL-Theorem-Prover/HOL)

Utility functions and tactics for HOL4

HOL4 formalization of a theory of specifications, components, contracts, and compositionality

A port of the default vim configuration shipped with HOL4 to Neovim, for users of lazy.nvim.

My solutions for the KTH HOL4 course - Interactive Theorem Proving