isabelle
There are 79 repositories under isabelle topic.
seL4/l4v
seL4 specification and proofs
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
diekmann/Iptables_Semantics
Verified iptables Firewall Ruleset Analysis
nunchaku-inria/nunchaku
Model finder for higher-order logic
dominique-unruh/scala-isabelle
A Scala library for controlling/interacting with Isabelle
larsrh/libisabelle
A Scala library which talks to Isabelle (DISCONTINUED)
isabelle-utp/utp-main
An implementation of Hoare and He's Unifying Theories of Programming in Isabelle
jaycech3n/Isabelle-HoTT
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
wimmers/munta
Fully verified model checker for realtime systems
uqcyber/veriopt-releases
Verifying the optimization phases of the GraalVM compiler
inpefess/isabelle-client
A client for Isabelle server (https://isabelle.in.tum.de)
tobias-rothmann/Polynomial-Commitment-Schemes
Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.
BaseMax/IssabelWebservicePHP
ISSABEL simple API Restful JSON: Provide call history reports from Issabel for a Call center powered by PHP with a JSON web-service interface
rohitdureja/isabelle-practice
Exercises from the Prog-Prove manual of Isabelle
jaycech3n/Isabelle-Spartan
A dependent type theory logic for Isabelle
ThreeFx/isabelle.vim
NeoVim extension used in conjunction with coc-isabelle
jvanbruegge/binder_datatypes
A new foundational package for Isabelle/HOL that implements binding-aware datatypes
ThreeFx/coc-isabelle
Because PIDE is not my editor.
appliedfm/growth-data
Measuring the growth of open source formal methods
seanpm2001/SNU_2D_ProgrammingTools_IDE_IsabelleProofAssistant
The Isabelle Proof-assistant language IDE submodule for SNU Programming Tools (2D Mode)
juanbono/concrete-semantics-exercises
Learning Isabelle/HOL
larsrh/purely-experimental
Experiments in Isabelle/Pure (and a bit of HOL) (ARCHIVED)
Pinpickle/matapaki-lang
Alternative EVM smart contract language
tarc/concrete-semantics-book
Self study log of the book
ThomasHickman/Isabelle-CAS-Integration
A project to integrate the functionality of Computer Algebra Systems into Isabelle
input-output-hk/equivalence-reasoner
An automated equivalence reasoner for Isabelle/HOL
joewatt95/CVM
Code repository for the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant"
kappelmann/SpecCheck
QuickCheck-like testing framework for Isabelle/ML
Kuniwak/isabelle-git-commit-graph
Formal Definition of the Git Commit‑Graph Model
larsrh/phd-thesis
LaTeX sources of my PhD thesis (ARCHIVED)
logicalhacking/Isabelle_DOF
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.
lukaskollmer/advent-of-code
Advent of Code solutions, in OCaml and (sometimes) Isabelle/HOL
nielstron/bplustrees
A Verified Imperative Implementation of B+-Trees in Isabelle
seanpm2001/AI2001_Category-Source_Code-SC-Isabelle
🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:Isabelle category for AI2001, containing Isabelle programming language datasets
seanpm2001/Learn-Isabelle
A repository for showcasing my knowledge of the Isabelle Mathematical Proofing Programming language, and continuing to learn the language.