diff --git a/AI_GUIDELINES.md b/AI_GUIDELINES.md
new file mode 100644
index 000000000..a790d9d27
--- /dev/null
+++ b/AI_GUIDELINES.md
@@ -0,0 +1,13 @@
+# Generative AI Guidelines
+AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. 
+Please carefully review your code to ensure it meets the following standards.
+
+- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
+- `have` statements that do not aid readability or code reuse should be inlined. 
+- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
+- In general, proofs should not perform substantially more case splitting than their Rocq counterparts.
+
+In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. 
+We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. 
+
+
diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml
index 2239fdc58..6c39df2ac 100644
--- a/Iris/lakefile.toml
+++ b/Iris/lakefile.toml
@@ -1,5 +1,6 @@
 name = "iris"
 defaultTargets = ["Iris", "IrisTest"]
+lintDriver = "batteries/runLinter"
 
 [[require]]
 name = "Qq"
diff --git a/PULL_REQUEST_TEMPLATE.md b/PULL_REQUEST_TEMPLATE.md
index 6ae23494e..685779f6b 100644
--- a/PULL_REQUEST_TEMPLATE.md
+++ b/PULL_REQUEST_TEMPLATE.md
@@ -6,15 +6,5 @@ Fixes # (issue number)
 ## Checklist
 * [ ] My code follows the mathlib [naming](https://leanprover-community.github.io/contribute/naming.html) and [code style](https://leanprover-community.github.io/contribute/style.html) conventions
 * [ ] I have added my name to the `authors` section of any appropriate files
-
-## Generative AI Guidelines
-AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. 
-Please carefully review your code to ensure it meets the following standards.
-
-- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
-- `have` statements that do not aid readability or code reuse should be inlined. 
-- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
-- In general, proofs should not perform substantially more case splitting than their Rocq counterparts.
-
-In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. 
-We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. 
+* [ ] My code passes the linter (`lake lint`)
+* [ ] I have followed the Iris-Lean generative AI guidelines, as outlined in [AI_GUIDELINES.md](https://github.com/leanprover-community/iris-lean/blob/master/AI_GUIDELINES.md)