  We introduce our implementation in HOL Light of the metatheory for
G\"odel-L\"ob provability logic (GL), covering soundness and completeness
w.r.t. possible world semantics and featuring a prototype of a theorem prover
for GL itself. The strategy we develop here to formalise the modal completeness
proof overcomes the technical difficulty due to the non-compactness of GL and
is an adaptation -- according to the formal language and tools at hand -- of
the proof given in George Boolos' 1995 monograph. Our theorem prover for GL
relies then on this formalisation, is implemented as a tactic of HOL Light that
mimics the proof search in the labelled sequent calculus G3KGL, and works as a
decision algorithm for the provability logic: if the algorithm positively
terminates, the tactic succeeds in producing a HOL Light theorem stating that
the input formula is a theorem of GL; if the algorithm negatively terminates,
the tactic extracts a model falsifying the input formula. We discuss our code
for the formal proof of modal completeness and the design of our proof search
algorithm. Furthermore, we propose some examples of the latter's interactive
and automated use.
