diff --git a/lkql_checker/doc/gnatcheck_rm/list_of_rules.rst b/lkql_checker/doc/gnatcheck_rm/list_of_rules.rst
index de63ea595..8f44b688d 100644
--- a/lkql_checker/doc/gnatcheck_rm/list_of_rules.rst
+++ b/lkql_checker/doc/gnatcheck_rm/list_of_rules.rst
@@ -61,6 +61,7 @@ GNATcheck rules.
 * :ref:`Explicit_Full_Discrete_Ranges`
 * :ref:`Explicit_Inlining`
 * :ref:`Expression_Functions`
+* :ref:`Final_Package`
 * :ref:`Fixed_Equality_Checks`
 * :ref:`Float_Equality_Checks`
 * :ref:`Forbidden_Aspects`
diff --git a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst b/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
index 8cf5990b5..84db9dcea 100644
--- a/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
+++ b/lkql_checker/doc/gnatcheck_rm/predefined_rules.rst
@@ -2651,6 +2651,31 @@ This rule has the following (optional) parameter for the ``+R`` option:
    end Bar;
 
 
+.. _Final_Package:
+
+``Final_Package``
+^^^^^^^^^^^^^^^^^
+
+Check that package declarations annotated as final don't have child
+packages
+
+.. note:: We don't do a transitive check, so grandchild packages won't
+   be flagged. We consider this is not necessary, because the child
+   package will be flagged anyway.
+
+Here is an example:
+
+   .. code-block:: ada
+
+      package Pkg with Annotate => (GNATcheck, Final) is
+      end Pkg;
+
+      package Pkg.Child is -- FLAG
+      end Pkg.Child;
+
+      package Pkg.Child.Grandchild is -- NOFLAG
+      end Pkg.Child.Grandchild;
+
 .. _Global_Variables:
 
 ``Global_Variables``