docs: align with documentation standards (metrics in CHANGELOG)

README:
- Update SPARK Results field to reference CHANGELOG
- Update SPARK Proof Coverage section to reference CHANGELOG

STG:
- Use [N] placeholders in expected output
- Remove specific test counts from Section 11.1
- Replace Section 11.3 v3.0.0 Test Additions with CHANGELOG reference
- Add test_scoped.adb to test file table

SRS:
- Project Statistics section previously removed

Per documentation agent Metrics vs Requirements rule:
- README contains high-level status
- CHANGELOG contains per-release metrics (single source of truth)

Author: abitofhelp

CHANGELOG.md

@@ -83,6 +83,9 @@ Val := Int_Result.Unwrap_Or (R, Default_Value);
 ### Technical Details
 - All 269 unit tests passing
 - SPARK proved (Option, Result, Either, Version)
+- **SPARK proof coverage**: 402 checks, 401 proved (99.7%), 270 subprograms analyzed
+  - Comprehensive instantiation tests (`test/spark/`) exercise all generic operations
+  - All helper functions proven overflow-safe
 - Scoped uses SPARK_Mode => Off (requires Ada.Finalization)
 - Zero heap allocation maintained
 

README.md

@@ -24,15 +24,15 @@ Designed for safety-critical, embedded, and high-assurance applications with ful
 </tr>
 <tr>
 <td><strong>Scope</strong></td>
-<td>All packages (Option, Result, Either, Version)</td>
+<td>All packages (Option, Result, Either, Version) + comprehensive instantiation tests</td>
 </tr>
 <tr>
 <td><strong>Mode</strong></td>
 <td>gnatprove --mode=prove --level=2 (full proof)</td>
 </tr>
 <tr>
 <td><strong>Results</strong></td>
-<td>76 checks: 40 flow, 36 proved, 0 unproved</td>
+<td>See <a href="CHANGELOG.md">CHANGELOG</a> for current proof statistics</td>
 </tr>
 </table>
 
@@ -63,6 +63,14 @@ make spark-prove    # Run full SPARK proof verification
 
 The `Try` and `Scoped` modules use `SPARK_Mode => Off` because they interact with exception handling and finalization respectively.
 
+### SPARK Proof Coverage
+
+Since SPARK only analyzes instantiated generics (not generic templates), the library includes a comprehensive SPARK test suite (`test/spark/`) that instantiates all generic operations, providing:
+
+- **Full operation coverage**: All Map, And_Then, Filter, Zip, Flatten, Fold operations instantiated
+- **Helper function verification**: All predicates and transformers formally proven overflow-safe
+- **High proof rate**: See [CHANGELOG](CHANGELOG.md) for current statistics
+
 ## Features
 
 ### Core Types (85+ operations)

docs/formal/software_requirements_specification.md

@@ -370,15 +370,7 @@ None - pure library with no hardware dependencies.
 | Functional.Try | 5 functions |
 | **Total** | **87 operations** |
 
-### 7.2 Project Statistics
-
-- Source Files: 13
-- Test Files: 6
-- Total Tests: 227
-- Code Coverage: 95% (stmt+decision)
-- SPARK Packages: 3 (Option, Result, Either)
-
-### 7.3 v3.0.0 Breaking Changes Summary
+### 7.2 v3.0.0 Breaking Changes Summary
 
 | Change | Old (2.x) | New (3.0.0) |
 |--------|-----------|-------------|

docs/formal/software_test_guide.md

@@ -129,18 +129,20 @@ Functional Library - Unit Test Suite
 ========================================
         GRAND TOTAL - ALL UNIT TESTS
 ========================================
-Total tests:   227
-Passed:        227
+Total tests:   [N]
+Passed:        [N]
 Failed:        0
 
 ########################################
 ###
 ###    UNIT TESTS: SUCCESS
-###    All  227 tests passed!
+###    All [N] tests passed!
 ###
 ########################################
 ```
 
+*Note: [N] represents current test counts. See CHANGELOG for actual values.*
+
 ## 5. Writing Tests
 
 ### 5.1 Test File Structure
@@ -457,16 +459,18 @@ Each test file header should include:
 
 ## 11. Test Statistics
 
-### 11.1 Current Test Counts
+### 11.1 Test Counts
+
+See [CHANGELOG](../../CHANGELOG.md) for current test counts per release.
 
-| Test File | Tests | Target Package |
-|-----------|-------|----------------|
-| test_result.adb | 84 | Functional.Result (36 operations) |
-| test_option.adb | 65 | Functional.Option (26 operations) |
-| test_either.adb | 58 | Functional.Either (20 operations) |
-| test_try.adb | 14 | Functional.Try (5 functions) |
-| test_try_option.adb | 6 | Try Option bridges |
-| **Total** | **227** | **87 operations** |
+| Test File | Target Package |
+|-----------|----------------|
+| test_result.adb | Functional.Result |
+| test_option.adb | Functional.Option |
+| test_either.adb | Functional.Either |
+| test_try.adb | Functional.Try |
+| test_try_option.adb | Try Option bridges |
+| test_scoped.adb | Functional.Scoped |
 
 ### 11.2 Test Commands Reference
 
@@ -478,35 +482,6 @@ Each test file header should include:
 | `make clean-test` | Clean test artifacts |
 | `./test/bin/unit_runner` | Run tests directly |
 
-### 11.3 v3.0.0 Test Additions
-
-The following operations were added in v3.0.0 and have full test coverage:
-
-**Result tests added:**
-- `Contains` / `"="` operator
-- `Is_Ok_And`, `Is_Error_And` (strict predicates)
-- `Is_Ok_Or`, `Is_Error_Or` (lenient predicates)
-- `Expect_Error`, `Unwrap_Error`
-- `Map_Or`, `Map_Or_Else`
-- `Tap_Ok`, `Tap_Error`
-- `Zip_With`, `Flatten`, `To_Option`
-
-**Option tests added:**
-- `Contains` / `"="` operator
-- `Is_Some_And` (strict predicate)
-- `Is_None_Or` (lenient predicate)
-- `Expect`
-- `Map_Or`, `Map_Or_Else`
-- `Tap`
-- `"and"`, `"xor"` operators
-- `Zip_With`, `Flatten`
-- `Ok_Or`, `Ok_Or_Else`
-
-**Either tests added:**
-- `Contains` / `"="` operator
-- `Is_Left_And`, `Is_Right_And` (strict predicates)
-- `Is_Left_Or`, `Is_Right_Or` (lenient predicates)
-- `Get_Or_Else`
-- `Map`, `Swap`, `And_Then`
-- `Merge`
-- `To_Option`, `To_Result`
+### 11.3 Version-Specific Changes
+
+See [CHANGELOG](../../CHANGELOG.md) for test additions and changes per release.