diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0101c29..e4aa06c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,14 +25,27 @@ jobs:
         with:
           version: 1.2.0
 
-      - name: Build
+      - name: Build library
         run: alr build --validation
 
-      - name: Unit tests
+      - name: Build and run unit tests (instrumented)
+        run: |
+          cd tests
+          alr gnatcov instrument --level=stmt+mcdc --dump-trigger=atexit --projects cobs.gpr
+          alr build -- --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts_full
+          alr exec -- bin/unit_tests
+          alr gnatcov coverage --annotate=xcov --output-dir gnatcov_out --level=stmt+mcdc --projects cobs.gpr *.srctrace
+
+      - name: Build and run unit tests (non-instrumented)
         run: |
           cd tests
           alr build --validation
-          alr run
+          alr exec -- bin/unit_tests
+
+      - uses: alire-project/gnatcov-to-codecovio-action@main
+        with:
+          fail_ci_if_error: false # Don't fail the workflow if codecov.io failed
+          verbose: true
 
       - name: Proof
         run: |
diff --git a/README.md b/README.md
index 96aaf72..3db2d8f 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Consistent Overhead Byte Stuffing (COBS)
 This repository provides an implementation of a COBS[1] encoder and
-decoder using the SPARK programming language. 
+decoder using the SPARK programming language.
 
 ## License
 All files are licensed under the MIT license.
@@ -55,11 +55,54 @@ is
 
    type My_COBS is new Generic_COBS (Byte       => Unsigned_8,
                                      Index      => Positive,
-                                     Byte_Count => Positive,
+                                     Byte_Count => Natural,
                                      Byte_Array => Byte_Array);
 end Example;
 ```
 
+## Verification
+
+This project takes a "hybrid verification" approach combining formal
+verification and testing.
+
+GNATprove is used to prove absence of run-time errors. At the time of writing
+there are 139 checks that are automatically proved.
+
+The unit tests are used to check that the encoder and decoder produce the
+correct results for a variety of inputs, with 100% MC/DC source coverage.
+
+### Reproducing the results
+
+#### Proof
+
+To run the proofs:
+
+```sh
+cd prove
+alr exec -- gnatprove -P ../cobs
+```
+
+If you want to see only failed checks, then pass `--report=fail` to `gnatprove`.
+
+#### Tests
+
+To run the unit tests:
+```sh
+alr build --verification
+cd tests
+alr build --verification
+alr run
+```
+
+To run the tests and generate a code coverage report:
+```sh
+alr build --verification
+cd tests
+./coverage.sh
+```
+
+The report will be generated in `tests/gnatcov_out/index.html`.
+
 ## References
 
 [1] Consistent Overheady Byte Stuffing
diff --git a/src/generic_cobs.adb b/src/generic_cobs.adb
index 7c77cb9..c509f00 100644
--- a/src/generic_cobs.adb
+++ b/src/generic_cobs.adb
@@ -60,8 +60,6 @@ is
 
             Code       := B;
             Run_Length := Byte_Count (Byte'Pos (B));
-
-            exit when B = Frame_Delimiter;
          end if;
 
          Run_Length := Run_Length - 1;
diff --git a/tests/.gitignore b/tests/.gitignore
index 5866d7b..79628df 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -2,3 +2,5 @@
 /bin/
 /alire/
 /config/
+*.srctrace
+/gnatcov_out/
\ No newline at end of file
diff --git a/tests/alire.toml b/tests/alire.toml
index 75fe775..0f52077 100644
--- a/tests/alire.toml
+++ b/tests/alire.toml
@@ -10,7 +10,8 @@ executables = ["unit_tests"]
 
 [[depends-on]]
 aunit = "^22.0.0"
+gnatcov = "^22.0.1"
 cobs = "*"
 
 [[pins]]
-cobs = { path = "../" }
\ No newline at end of file
+cobs = { path = "../" }
diff --git a/tests/coverage.sh b/tests/coverage.sh
new file mode 100644
index 0000000..02a88e1
--- /dev/null
+++ b/tests/coverage.sh
@@ -0,0 +1,14 @@
+#!/bin/sh
+
+alr gnatcov instrument --level=stmt+mcdc --dump-trigger=atexit --projects cobs.gpr
+
+alr build -- --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts_full
+
+alr exec -- bin/unit_tests
+
+alr gnatcov coverage \
+    --annotate=html+ \
+    --output-dir gnatcov_out \
+    --level=stmt+mcdc \
+    --projects cobs.gpr \
+    *.srctrace
\ No newline at end of file
diff --git a/tests/run_tests.sh b/tests/run_tests.sh
deleted file mode 100755
index ecb2be1..0000000
--- a/tests/run_tests.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-
-gprbuild -p -P unit_tests.gpr -j0
-obj/main
\ No newline at end of file
diff --git a/tests/src/cobs_tests.adb b/tests/src/cobs_tests.adb
index 01b73a2..61effb6 100644
--- a/tests/src/cobs_tests.adb
+++ b/tests/src/cobs_tests.adb
@@ -269,6 +269,177 @@ is
       end loop;
    end Test_Encode_Decode_Loopback;
 
+   -------------------------------------------
+   -- Test_Array_Upper_Limit_Positive_Range --
+   -------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns True when given the
+   --  largest allowed range across positive values.
+
+   procedure Test_Array_Upper_Limit_Positive_Range (T : in out Test) is
+   begin
+      Assert (COBS.Array_Length_Within_Bounds (1, Storage_Offset'Last),
+              "Check unexpectedly failed");
+   end Test_Array_Upper_Limit_Positive_Range;
+
+   -------------------------------------------
+   -- Test_Array_Upper_Limit_Negative_Range --
+   -------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns True when given the
+   --  largest allowed range across negative values.
+
+   procedure Test_Array_Upper_Limit_Negative_Range (T : in out Test) is
+   begin
+      Assert (COBS.Array_Length_Within_Bounds (Storage_Offset'First, -2),
+              "Check unexpectedly failed");
+   end Test_Array_Upper_Limit_Negative_Range;
+
+   ------------------------------------------------
+   -- Test_Array_Upper_Limit_Zero_Crossing_Range --
+   ------------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns True when given the
+   --  largest allowed range symmetrically across zero values.
+
+   procedure Test_Array_Upper_Limit_Zero_Crossing_Range (T : in out Test) is
+      First : constant Storage_Offset := Storage_Offset'First / 2;
+      Last  : constant Storage_Offset := First + Storage_Offset'Last - 1;
+
+   begin
+      Assert (COBS.Array_Length_Within_Bounds (First, Last),
+              "Check unexpectedly failed");
+   end Test_Array_Upper_Limit_Zero_Crossing_Range;
+
+   -------------------------------------------
+   -- Test_Bounds_Exceeded_Positive_Range --
+   -------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns False when given
+   --  a positive range that is one past the maximum allowed length.
+
+   procedure Test_Bounds_Exceeded_Positive_Range (T : in out Test) is
+   begin
+      Assert (not COBS.Array_Length_Within_Bounds (0, Storage_Offset'Last),
+              "Check unexpectedly succeeded");
+   end Test_Bounds_Exceeded_Positive_Range;
+
+   -------------------------------------------
+   -- Test_Bounds_Exceeded_Negative_Range --
+   -------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns False when given
+   --  a negative range that is one past the maximum allowed length.
+
+   procedure Test_Bounds_Exceeded_Negative_Range (T : in out Test) is
+   begin
+      Assert (not COBS.Array_Length_Within_Bounds (Storage_Offset'First, -1),
+              "Check unexpectedly succeeded");
+   end Test_Bounds_Exceeded_Negative_Range;
+
+   ------------------------------------------------
+   -- Test_Bounds_Exceeded_Zero_Crossing_Range --
+   ------------------------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns False when given
+   --  a range crossing zero that is one past the maximum allowed length.
+
+   procedure Test_Bounds_Exceeded_Zero_Crossing_Range (T : in out Test) is
+      First : constant Storage_Offset := Storage_Offset'First / 2;
+      Last  : constant Storage_Offset := First + Storage_Offset'Last;
+   begin
+      Assert (not COBS.Array_Length_Within_Bounds (First, Last),
+              "Check unexpectedly succeeded");
+   end Test_Bounds_Exceeded_Zero_Crossing_Range;
+
+   -----------------------------------
+   -- Test_Bounds_Check_Empty_Range --
+   -----------------------------------
+
+   --  Test that Array_Length_Within_Bounds returns True when given
+   --  an empty/null range.
+
+   procedure Test_Bounds_Check_Empty_Range (T : in out Test) is
+   begin
+      Assert (COBS.Array_Length_Within_Bounds (0, -1),
+              "Check unexpectedly failed");
+   end Test_Bounds_Check_Empty_Range;
+
+   -----------------------------------
+   -- Test_Max_Overhead_Bytes_Empty --
+   -----------------------------------
+
+   --  Test Max_Overhead_Bytes with length zero.
+
+   procedure Test_Max_Overhead_Bytes_Empty (T : in out Test) is
+      Result : Storage_Count;
+   begin
+      Result := COBS.Max_Overhead_Bytes (0);
+      Assert (Result = 1,
+              "Incorrect overhead bytes count:" &
+                Storage_Count'Image (Result));
+   end Test_Max_Overhead_Bytes_Empty;
+
+   ---------------------------------------------
+   -- Test_Max_Overhead_Bytes_Under_One_Block --
+   ---------------------------------------------
+
+   --  Test Max_Overhead_Bytes with length of one byte under one block.
+
+   procedure Test_Max_Overhead_Bytes_Under_One_Block (T : in out Test) is
+      Result : Storage_Count;
+   begin
+      Result := COBS.Max_Overhead_Bytes (253);
+      Assert (Result = 1,
+              "Incorrect overhead bytes count:" &
+                Storage_Count'Image (Result));
+   end Test_Max_Overhead_Bytes_Under_One_Block;
+
+   ---------------------------------------
+   -- Test_Max_Overhead_Bytes_One_Block --
+   ---------------------------------------
+
+   --  Test Max_Overhead_Bytes with length of exactly one block.
+
+   procedure Test_Max_Overhead_Bytes_One_Block (T : in out Test) is
+      Result : Storage_Count;
+   begin
+      Result := COBS.Max_Overhead_Bytes (254);
+      Assert (Result = 2,
+              "Incorrect overhead bytes count:" &
+                Storage_Count'Image (Result));
+   end Test_Max_Overhead_Bytes_One_Block;
+
+   ----------------------------------------
+   -- Test_Max_Overhead_Bytes_Over_Block --
+   ----------------------------------------
+
+   --  Test Max_Overhead_Bytes with length of one byte more than one block.
+
+   procedure Test_Max_Overhead_Bytes_Over_Block (T : in out Test) is
+      Result : Storage_Count;
+   begin
+      Result := COBS.Max_Overhead_Bytes (255);
+      Assert (Result = 2,
+              "Incorrect overhead bytes count:" &
+                Storage_Count'Image (Result));
+   end Test_Max_Overhead_Bytes_Over_Block;
+
+   ----------------------------------------
+   -- Test_Max_Overhead_Bytes_Two_Blocks --
+   ----------------------------------------
+
+   --  Test Max_Overhead_Bytes with length of exactly two blocks.
+
+   procedure Test_Max_Overhead_Bytes_Two_Blocks (T : in out Test) is
+      Result : Storage_Count;
+   begin
+      Result := COBS.Max_Overhead_Bytes (254 * 2);
+      Assert (Result = 3,
+              "Incorrect overhead bytes count:" &
+                Storage_Count'Image (Result));
+   end Test_Max_Overhead_Bytes_Two_Blocks;
+
    -----------
    -- Suite --
    -----------
@@ -277,28 +448,63 @@ is
    is
       Ret : constant Access_Test_Suite := new Test_Suite;
    begin
-      Ret.Add_Test
-        (Test_Caller.Create ("Encode an empty array",
-                             Test_Encode_Empty'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Encode an array of all zeroes",
-                             Test_Encode_All_Zeroes'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Encode an array of no zeroes",
-                             Test_Encode_No_Zeroes'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Decode an empty frame",
-                             Test_Decode_Empty_Frame'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Decode a frame with a missing frame delimiter",
-                             Test_Decode_No_Frame_Delimiter'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Decode test vectors",
-                             Test_Decode_Test_Vectors'Access));
-      Ret.Add_Test
-        (Test_Caller.Create ("Encode/decode loopback",
-                             Test_Encode_Decode_Loopback'Access));
-
+      Ret.Add_Test (Test_Caller.Create
+                      ("Encode an empty array",
+                       Test_Encode_Empty'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Encode an array of all zeroes",
+                       Test_Encode_All_Zeroes'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Encode an array of no zeroes",
+                       Test_Encode_No_Zeroes'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Decode an empty frame",
+                       Test_Decode_Empty_Frame'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Decode a frame with a missing frame delimiter",
+                       Test_Decode_No_Frame_Delimiter'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Decode test vectors",
+                       Test_Decode_Test_Vectors'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Encode/decode loopback",
+                       Test_Encode_Decode_Loopback'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check upper limit (positive range)",
+                       Test_Array_Upper_Limit_Positive_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check upper limit (negative range)",
+                       Test_Array_Upper_Limit_Negative_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check upper limit (zero-crossing range)",
+                       Test_Array_Upper_Limit_Zero_Crossing_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check 1 past limit (positive range)",
+                       Test_Bounds_Exceeded_Positive_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check 1 past limit (negative range)",
+                       Test_Bounds_Exceeded_Negative_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check 1 past limit (zero-crossing range)",
+                       Test_Bounds_Exceeded_Zero_Crossing_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test bounds check (empty range)",
+                       Test_Bounds_Check_Empty_Range'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test overhead bytes with 0 length",
+                       Test_Max_Overhead_Bytes_Empty'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test overhead bytes with just under one block",
+                       Test_Max_Overhead_Bytes_Under_One_Block'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test overhead bytes with exactly one block",
+                       Test_Max_Overhead_Bytes_One_Block'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test overhead bytes with just over one block",
+                       Test_Max_Overhead_Bytes_Over_Block'Access));
+      Ret.Add_Test (Test_Caller.Create
+                      ("Test overhead bytes with exactly two blocks",
+                       Test_Max_Overhead_Bytes_Two_Blocks'Access));
       return Ret;
    end Suite;
 
diff --git a/tests/src/cobs_tests.ads b/tests/src/cobs_tests.ads
index 3a9e15a..ba10d49 100644
--- a/tests/src/cobs_tests.ads
+++ b/tests/src/cobs_tests.ads
@@ -49,6 +49,28 @@ is
 
    procedure Test_Encode_Decode_Loopback (T : in out Test);
 
+   ----------------------------------------
+   --  Array_Length_Within_Bounds tests  --
+   ----------------------------------------
+
+   procedure Test_Array_Upper_Limit_Positive_Range (T : in out Test);
+   procedure Test_Array_Upper_Limit_Negative_Range (T : in out Test);
+   procedure Test_Array_Upper_Limit_Zero_Crossing_Range (T : in out Test);
+   procedure Test_Bounds_Exceeded_Positive_Range (T : in out Test);
+   procedure Test_Bounds_Exceeded_Negative_Range (T : in out Test);
+   procedure Test_Bounds_Exceeded_Zero_Crossing_Range (T : in out Test);
+   procedure Test_Bounds_Check_Empty_Range (T : in out Test);
+
+   --------------------------------
+   --  Max_Overhead_Bytes tests  --
+   --------------------------------
+
+   procedure Test_Max_Overhead_Bytes_Empty (T : in out Test);
+   procedure Test_Max_Overhead_Bytes_Under_One_Block (T : in out Test);
+   procedure Test_Max_Overhead_Bytes_One_Block (T : in out Test);
+   procedure Test_Max_Overhead_Bytes_Over_Block (T : in out Test);
+   procedure Test_Max_Overhead_Bytes_Two_Blocks (T : in out Test);
+
    ----------------
    -- Test suite --
    ----------------