diff --git a/Arm.lean b/Arm.lean
index 95b9825f..9ca0c6ce 100644
--- a/Arm.lean
+++ b/Arm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Arm` library.
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index b84df467..e64217c6 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 
diff --git a/Arm/Cfg/Cfg.lean b/Arm/Cfg/Cfg.lean
index b83acbf5..639cd37e 100644
--- a/Arm/Cfg/Cfg.lean
+++ b/Arm/Cfg/Cfg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Arm/Cosim.lean b/Arm/Cosim.lean
index 0cee31a6..379333f8 100644
--- a/Arm/Cosim.lean
+++ b/Arm/Cosim.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Arm/Decode.lean b/Arm/Decode.lean
index 4a956d9f..de45525d 100644
--- a/Arm/Decode.lean
+++ b/Arm/Decode.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Memory
diff --git a/Arm/Decode/BR.lean b/Arm/Decode/BR.lean
index 29b69b29..a3908560 100644
--- a/Arm/Decode/BR.lean
+++ b/Arm/Decode/BR.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
diff --git a/Arm/Decode/DPI.lean b/Arm/Decode/DPI.lean
index 2783532a..7ee2a37c 100644
--- a/Arm/Decode/DPI.lean
+++ b/Arm/Decode/DPI.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean
index 4ca7f2f3..4a82dcb9 100644
--- a/Arm/Decode/DPR.lean
+++ b/Arm/Decode/DPR.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean
index c795552f..dab3789f 100644
--- a/Arm/Decode/DPSFP.lean
+++ b/Arm/Decode/DPSFP.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Arm/Decode/LDST.lean b/Arm/Decode/LDST.lean
index 89b6313e..6355c9f4 100644
--- a/Arm/Decode/LDST.lean
+++ b/Arm/Decode/LDST.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Arm/Exec.lean b/Arm/Exec.lean
index 9ad033ef..0e71305a 100644
--- a/Arm/Exec.lean
+++ b/Arm/Exec.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Arm/Insts.lean b/Arm/Insts.lean
index 400603a9..68350528 100644
--- a/Arm/Insts.lean
+++ b/Arm/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPI.Insts
diff --git a/Arm/Insts/BR/Compare_branch.lean b/Arm/Insts/BR/Compare_branch.lean
index 87bd4054..3e2529da 100644
--- a/Arm/Insts/BR/Compare_branch.lean
+++ b/Arm/Insts/BR/Compare_branch.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 
diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean
index 6df81d1f..87f8762f 100644
--- a/Arm/Insts/BR/Cond_branch_imm.lean
+++ b/Arm/Insts/BR/Cond_branch_imm.lean
@@ -1,5 +1,6 @@
-/-+
+/-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 
diff --git a/Arm/Insts/BR/Insts.lean b/Arm/Insts/BR/Insts.lean
index 06fffc78..81955d06 100644
--- a/Arm/Insts/BR/Insts.lean
+++ b/Arm/Insts/BR/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.BR.Compare_branch
diff --git a/Arm/Insts/BR/Uncond_branch_imm.lean b/Arm/Insts/BR/Uncond_branch_imm.lean
index 41389c1f..56efd9f4 100644
--- a/Arm/Insts/BR/Uncond_branch_imm.lean
+++ b/Arm/Insts/BR/Uncond_branch_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 
diff --git a/Arm/Insts/BR/Uncond_branch_reg.lean b/Arm/Insts/BR/Uncond_branch_reg.lean
index 384d6741..7b8ffdcb 100644
--- a/Arm/Insts/BR/Uncond_branch_reg.lean
+++ b/Arm/Insts/BR/Uncond_branch_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 
diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index 2e8b0611..87ccae4b 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
diff --git a/Arm/Insts/Cosim/disasm.sh b/Arm/Insts/Cosim/disasm.sh
index ff10cdfd..8e33d49b 100755
--- a/Arm/Insts/Cosim/disasm.sh
+++ b/Arm/Insts/Cosim/disasm.sh
@@ -1,4 +1,5 @@
 # Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 #!/bin/sh
diff --git a/Arm/Insts/Cosim/platform_check.sh b/Arm/Insts/Cosim/platform_check.sh
index bf7b5b93..d56a2707 100755
--- a/Arm/Insts/Cosim/platform_check.sh
+++ b/Arm/Insts/Cosim/platform_check.sh
@@ -1,4 +1,5 @@
 # Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 #!/bin/bash
diff --git a/Arm/Insts/DPI/Add_sub_imm.lean b/Arm/Insts/DPI/Add_sub_imm.lean
index 329247ad..3b840669 100644
--- a/Arm/Insts/DPI/Add_sub_imm.lean
+++ b/Arm/Insts/DPI/Add_sub_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADD, ADDS, SUB, SUBS (immediate): 32- and 64-bit versions
diff --git a/Arm/Insts/DPI/Insts.lean b/Arm/Insts/DPI/Insts.lean
index 03689a3c..d07d2fcf 100644
--- a/Arm/Insts/DPI/Insts.lean
+++ b/Arm/Insts/DPI/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPI.Add_sub_imm
diff --git a/Arm/Insts/DPI/Logical_imm.lean b/Arm/Insts/DPI/Logical_imm.lean
index f17e3f6b..ae75ec70 100644
--- a/Arm/Insts/DPI/Logical_imm.lean
+++ b/Arm/Insts/DPI/Logical_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- AND, ORR, EOR, ANDS (immediate): 32- and 64-bit versions
diff --git a/Arm/Insts/DPI/PC_rel_addressing.lean b/Arm/Insts/DPI/PC_rel_addressing.lean
index f61af12f..0f2f9beb 100644
--- a/Arm/Insts/DPI/PC_rel_addressing.lean
+++ b/Arm/Insts/DPI/PC_rel_addressing.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADR, ADRP
diff --git a/Arm/Insts/DPR/Add_sub_carry.lean b/Arm/Insts/DPR/Add_sub_carry.lean
index ba6316d3..8f104fc6 100644
--- a/Arm/Insts/DPR/Add_sub_carry.lean
+++ b/Arm/Insts/DPR/Add_sub_carry.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADC, ADCS, SBC, SBCS: 32- and 64-bit versions
diff --git a/Arm/Insts/DPR/Add_sub_shifted_reg.lean b/Arm/Insts/DPR/Add_sub_shifted_reg.lean
index 9c97b3c8..eec61df9 100644
--- a/Arm/Insts/DPR/Add_sub_shifted_reg.lean
+++ b/Arm/Insts/DPR/Add_sub_shifted_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- ADD, ADDS, SUB, SUBS (shifted registers): 32- and 64-bit versions
diff --git a/Arm/Insts/DPR/Conditional_select.lean b/Arm/Insts/DPR/Conditional_select.lean
index 18f58e1a..fe262639 100644
--- a/Arm/Insts/DPR/Conditional_select.lean
+++ b/Arm/Insts/DPR/Conditional_select.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- CSEL, CSINC, CSINV, CSNEG: 32- and 64-bit versions
diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean
index d505ddd7..7dd42747 100644
--- a/Arm/Insts/DPR/Insts.lean
+++ b/Arm/Insts/DPR/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPR.Add_sub_carry
diff --git a/Arm/Insts/DPR/Logical_shifted_reg.lean b/Arm/Insts/DPR/Logical_shifted_reg.lean
index 9e12a77e..f3efbec2 100644
--- a/Arm/Insts/DPR/Logical_shifted_reg.lean
+++ b/Arm/Insts/DPR/Logical_shifted_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- AND, BIC, ORR, ORN, EOR, EON, ANDS, BICS: 32- and 64-bit versions
diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
index fe8f9788..5faa71eb 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- EXT
diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
index 09d15262..ba9d67f4 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 -- ADD, ORR, AND, BIC, ORR, ORN, EOR, BSL, BIT, BIF (vector)
diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
index 247fc656..dac34303 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- REV64
diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean
index e5ef266c..38631e73 100644
--- a/Arm/Insts/DPSFP/Crypto_aes.lean
+++ b/Arm/Insts/DPSFP/Crypto_aes.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- AESE, AESMC
diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
index 5be5f25d..333ddcc6 100644
--- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
+++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- SHA512H, SHA512H2, SHA512SU1
diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean
index f5d5641f..9574fdcc 100644
--- a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean
+++ b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- SHA512SU0
diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean
index 34d941c2..ce020ee1 100644
--- a/Arm/Insts/DPSFP/Insts.lean
+++ b/Arm/Insts/DPSFP/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc
diff --git a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
index d562b96f..0669caca 100644
--- a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
+++ b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDP, STP
diff --git a/Arm/Insts/LDST/Insts.lean b/Arm/Insts/LDST/Insts.lean
index f6507030..fcae55ed 100644
--- a/Arm/Insts/LDST/Insts.lean
+++ b/Arm/Insts/LDST/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.LDST.Reg_imm
diff --git a/Arm/Insts/LDST/Reg_imm.lean b/Arm/Insts/LDST/Reg_imm.lean
index ff6d476e..8b83571b 100644
--- a/Arm/Insts/LDST/Reg_imm.lean
+++ b/Arm/Insts/LDST/Reg_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDR/STR (immediate, SIMD&FP)
diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean
index 6e36574a..19da8339 100644
--- a/Arm/Insts/LDST/Reg_pair.lean
+++ b/Arm/Insts/LDST/Reg_pair.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDP, STP
diff --git a/Arm/Memory.lean b/Arm/Memory.lean
index 3414c39f..500f5abd 100644
--- a/Arm/Memory.lean
+++ b/Arm/Memory.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Separate
diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean
index 89d80460..e8b74a09 100644
--- a/Arm/MemoryProofs.lean
+++ b/Arm/MemoryProofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.SeparateProofs
diff --git a/Arm/Separate.lean b/Arm/Separate.lean
index 8dd2dc31..cd19b3bc 100644
--- a/Arm/Separate.lean
+++ b/Arm/Separate.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.State
diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean
index 5746851e..7cb8f057 100644
--- a/Arm/SeparateProofs.lean
+++ b/Arm/SeparateProofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Memory
diff --git a/Arm/State.lean b/Arm/State.lean
index e80d8a06..db565a8c 100644
--- a/Arm/State.lean
+++ b/Arm/State.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Main.lean b/Main.lean
index 464f5adc..90ef6bdf 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Arm»
diff --git a/Makefile b/Makefile
index a445ddb7..5f616b09 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,5 @@
 # Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 SHELL := /bin/bash
diff --git a/Proofs.lean b/Proofs.lean
index aaafe2d9..1060b980 100644
--- a/Proofs.lean
+++ b/Proofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Proofs` library.
diff --git a/Proofs/MultiInsts.lean b/Proofs/MultiInsts.lean
index bd5cfb77..e3276bc1 100644
--- a/Proofs/MultiInsts.lean
+++ b/Proofs/MultiInsts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Proofs/Proofs.lean b/Proofs/Proofs.lean
index da32c9c3..e9c27759 100644
--- a/Proofs/Proofs.lean
+++ b/Proofs/Proofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Proofs».MultiInsts
diff --git a/Proofs/SHA512_AssocRepr.lean b/Proofs/SHA512_AssocRepr.lean
index 579d1d41..9b9795cd 100644
--- a/Proofs/SHA512_AssocRepr.lean
+++ b/Proofs/SHA512_AssocRepr.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Proofs/Sha512_block_armv8.lean b/Proofs/Sha512_block_armv8.lean
index 9916d07d..938f1b64 100644
--- a/Proofs/Sha512_block_armv8.lean
+++ b/Proofs/Sha512_block_armv8.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Proofs/Sha512_block_armv8_rules.lean b/Proofs/Sha512_block_armv8_rules.lean
index 0ca2d6fa..4a802e1f 100644
--- a/Proofs/Sha512_block_armv8_rules.lean
+++ b/Proofs/Sha512_block_armv8_rules.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPSFP.Insts
diff --git a/Proofs/Test.lean b/Proofs/Test.lean
index 0daf0fb4..1735fe6e 100644
--- a/Proofs/Test.lean
+++ b/Proofs/Test.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean
index 5e068870..60ee0c56 100644
--- a/Specs/AESCommon.lean
+++ b/Specs/AESCommon.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Specs/SHA512.lean b/Specs/SHA512.lean
index 1b165f3c..311db5aa 100644
--- a/Specs/SHA512.lean
+++ b/Specs/SHA512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Std.Data.BitVec
diff --git a/Specs/SHA512Common.lean b/Specs/SHA512Common.lean
index e2f9a043..5048f86f 100644
--- a/Specs/SHA512Common.lean
+++ b/Specs/SHA512Common.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
diff --git a/Specs/Specs.lean b/Specs/Specs.lean
index 6dd6abb3..8ef481da 100644
--- a/Specs/Specs.lean
+++ b/Specs/Specs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Specs».SHA512
diff --git a/Tactics.lean b/Tactics.lean
index 66a3aedd..71e778ee 100644
--- a/Tactics.lean
+++ b/Tactics.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Tactics` library.
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index b0aabc90..d8a49b1c 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Tests.lean b/Tests.lean
index c09fa5ea..0542dfa4 100644
--- a/Tests.lean
+++ b/Tests.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Tests` library.
diff --git a/Tests/SHA512ProgramTest.lean b/Tests/SHA512ProgramTest.lean
index df04076a..0cb26e35 100644
--- a/Tests/SHA512ProgramTest.lean
+++ b/Tests/SHA512ProgramTest.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
diff --git a/Tests/SHA512SpecTest.lean b/Tests/SHA512SpecTest.lean
index 6313eead..4d38c3d1 100644
--- a/Tests/SHA512SpecTest.lean
+++ b/Tests/SHA512SpecTest.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Specs.SHA512
diff --git a/Tests/SHA512StandardSpecTest.lean b/Tests/SHA512StandardSpecTest.lean
index f574001f..9e14092b 100644
--- a/Tests/SHA512StandardSpecTest.lean
+++ b/Tests/SHA512StandardSpecTest.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Tests».SHA512SpecTest
diff --git a/Tests/Tests.lean b/Tests/Tests.lean
index 2f465eee..dba1cfc9 100644
--- a/Tests/Tests.lean
+++ b/Tests/Tests.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Tests».SHA512SpecTest