This is work in progress. Its ultimate goal is to formalise Abstraction Logic and its properties as described in Philosophy of Abstraction Logic and Abstraction Logic, using the proof assistant Isabelle, and in particular its logic Isabelle/HOL.
An outline of the current state of the formalisation is available here.
The current theories of the formalisation can be viewed here.