seL4 specification and proofs

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

Verified iptables Firewall Ruleset Analysis

Model finder for higher-order logic

A Scala library which talks to Isabelle (DISCONTINUED)

A Scala library for controlling/interacting with Isabelle

An implementation of Hoare and He's Unifying Theories of Programming in Isabelle

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

Fully verified model checker for realtime systems

Verifying the optimization phases of the GraalVM compiler

A client for Isabelle server (https://isabelle.in.tum.de)

Formalizing the KZG polynomial commitment scheme in the Interactive Theorem Prover Isabelle.

Exercises from the Prog-Prove manual of Isabelle

ISSABEL simple API Restful JSON: Provide call history reports from Issabel for a Call center powered by PHP with a JSON web-service interface

A dependent type theory logic for Isabelle

NeoVim extension used in conjunction with coc-isabelle

Because PIDE is not my editor.

Measuring the growth of open source formal methods

The Isabelle Proof-assistant language IDE submodule for SNU Programming Tools (2D Mode)