FazBrowse GitHub Viewer | Trending |
URL:
| Home
Tools: [Download Repo ZIP]   [Original HTTPS Page]

hol4 · GitHub Topics · GitHub

Explore Topics Trending Collections Events GitHub Sponsors
#

hol4

Star

Here are 12 public repositories matching this topic...

Language: All
Filter by language
All 12 Standard ML 9 Assembly 1 C 1 OCaml 1
Sort: Most stars
Sort options
Most stars Fewest stars Most forks Fewest forks Recently updated Least recently updated

AeneasVerif / aeneas

Star 929

A verification toolchain for Rust programs

rust compiler ocaml coq rust-lang lean formal-methods proofs program-verification formal-verification fstar hol4 deductive-reasoning
  • Updated Aug 28, 2026
  • OCaml

kth-step / HolBA

Star 47

Binary analysis in HOL

arm proof binary-analysis armv8 risc-v cortex-m0 hol4
  • Updated Aug 28, 2026
  • Standard ML

kth-step / HOL4P4

Star 20

P4 formalization using Ott and HOL4

ott p4 hol4
  • Updated Aug 5, 2026
  • Standard ML

kth-step / itppv-course

Star 14

Interactive Theorem Proving course using HOL4

course-materials hol4 cakeml
  • Updated Mar 27, 2026
  • Standard ML

palmskog / fitch

Star 7

Certified proof checker for Fitch-style propositional logic proofs

ocaml coq propositional-logic ott fitch-proofs hol4 cakeml
  • Updated Nov 21, 2023
  • Standard ML

kth-step / mil

Star 2

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

sml hol4 cakeml
  • Updated Oct 25, 2022
  • Standard ML

jimwhite / milawa-on-jitawa

Star 1

Ready-to-run copy of Milawa on Jitawa

formal-verification theorem-prover hol4 acl2
  • Updated Apr 8, 2026
  • Assembly

rse-verification / contract-compositionality

Star 0

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

contracts hol4
  • Updated May 2, 2025
  • Standard ML

tupipa / hol4-docker

Star 0

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

hol4
  • Updated Jun 23, 2017
  • Standard ML

kth-step / step-hol-utils

Star 0

Utility functions and tactics for HOL4

sml hol4
  • Updated Mar 10, 2021
  • Standard ML

totorigolo / kth-hol4-exercises

Star 0

My solutions for the KTH HOL4 course - Interactive Theorem Proving

sml latex-document kth hol4
  • Updated Feb 6, 2019
  • Standard ML

artisanbk / hol4nvim

Star 0

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

theorem-proving neovim-plugin hol4 lazyvim
  • Updated Jul 21, 2026
  • C

Improve this page

Add a description, image, and links to the hol4 topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the hol4 topic, visit your repo's landing page and select "manage topics."

Learn more

Back | FazBrowse Home | New Git URL