diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml
new file mode 100644
index 00000000..1863a250
--- /dev/null
+++ b/.github/workflows/copyright-header.yml
@@ -0,0 +1,20 @@
+name: Check for copyright header
+
+on: [pull_request]
+
+jobs:
+  check-lean-files:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Verify .lean files start with a copyright header.
+      run: |
+        FILES=$(find . -type d \( -path "./.lake" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+        if [ -n "$FILES" ]; then
+          echo "Found .lean files which do not have a copyright header:"
+          echo "$FILES"
+          exit 1
+        else
+          echo "All copyright headers present."
+        fi
\ No newline at end of file
diff --git a/Arm/Attr.lean b/Arm/Attr.lean
index fe2c434f..d9076b78 100644
--- a/Arm/Attr.lean
+++ b/Arm/Attr.lean
@@ -1,3 +1,9 @@
+/-
+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 Lean
 
 -- A minimal theory, safe for all LNSym proofs
@@ -9,21 +15,3 @@ register_simp_attr state_simp_rules
 register_simp_attr bitvec_rules
 -- Rules for memory lemmas
 register_simp_attr memory_rules
-
-/-
-syntax "state_simp" : tactic
-macro_rules
-  | `(tactic| state_simp) => `(tactic| simp only [state_simp_rules])
-
-syntax "state_simp?" : tactic
-macro_rules
-  | `(tactic| state_simp?) => `(tactic| simp? only [state_simp_rules])
-
-syntax "state_simp_all" : tactic
-macro_rules
-  | `(tactic| state_simp_all) => `(tactic| simp_all only [state_simp_rules])
-
-syntax "state_simp_all?" : tactic
-macro_rules
-  | `(tactic| state_simp_all?) => `(tactic| simp_all? only [state_simp_rules])
--/
diff --git a/Arm/FromMathlib.lean b/Arm/FromMathlib.lean
index 352537cf..3d17145f 100644
--- a/Arm/FromMathlib.lean
+++ b/Arm/FromMathlib.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+
 -- This file has definitions temporarily lifted from Mathlib.
 -- We will move them into Lean shortly.
 
diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean
index 602f47ee..a4cbc4fd 100644
--- a/Arm/MinTheory.lean
+++ b/Arm/MinTheory.lean
@@ -1,3 +1,9 @@
+/-
+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.Attr
 
 -- These lemmas are from lean/Init/SimpLemmas.lean.
diff --git a/Proofs/SHA512/SHA512.lean b/Proofs/SHA512/SHA512.lean
index 03709f50..f044c44e 100644
--- a/Proofs/SHA512/SHA512.lean
+++ b/Proofs/SHA512/SHA512.lean
@@ -1,2 +1,7 @@
+/-
+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 Proofs.SHA512.SHA512_block_armv8_rules
 import Proofs.SHA512.SHA512Sym
diff --git a/lakefile.lean b/lakefile.lean
index cc494af8..80f20126 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,3 +1,8 @@
+/-
+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 Lake
 open Lake DSL