Update the formal verification section in README

README.md

@@ -136,11 +136,29 @@ Portions of AWS-LC have been formally verified in
 [AWS-LC Formal Verification](https://github.com/awslabs/aws-lc-verification),
 the checks are run in AWS-LC’s CI on every change. The algorithms that have been
 verified on certain platforms with caveats include:
-* SHA-2
-* HMAC
-* AES-KWP
-* ECDH & ECDSA with curve P-384
-* HKDF
+| Algorithm | Variants | Platform   |
+| ----------| ------------| -----------
+| SHA-2 | 384, 512 | SandyBridge+ |
+| SHA-2 | 384 | neoverse-n1, neoverse-v1 |
+| HMAC | with <nobr>SHA-384</nobr> | SandyBridge+ |
+| <nobr>AES-KW(P)</nobr> | 256 | SandyBridge+ |
+| Elliptic Curve Keys and Parameters | with <nobr>P-384</nobr> | SandyBridge+ |
+| ECDSA | with <nobr>P-384</nobr>, <nobr>SHA-384</nobr> | SandyBridge+ |
+| ECDH | with <nobr>P-384</nobr> | SandyBridge+ |
+| HKDF | with <nobr>HMAC-SHA384</nobr> | SandyBridge+ |
+
+The platforms for which code is verified are defined in the following table.
+
+| Platform        | Description |
+| --------------- | ------------|
+| SandyBridge+ | x86-64 with AES-NI, CLMUL, and AVX.
+| SandyBridge-Skylake | x86-64 with AES-NI, CLMUL, and AVX, but not AVX-512.
+| neoverse-n1 | aarch64 without SHA512.
+| neoverse-v1 | aarch64 with SHA512.
+
+For more details on verified API functions, caveats and technology used, check the [AWS-LC Formal Verification](https://github.com/awslabs/aws-lc-verification) repository.
+
+In addition, we use assembly from [s2n-bignum](https://github.com/awslabs/s2n-bignum) for a subset of the big number arithmetic routines on x86_64 and aarch64. These routines are formally verified using HOL Light.
 
 ## Have a Question?