diff --git a/Research/courses.html b/Research/courses.html
index 3ce32cab2..d48f8ea3f 100644
--- a/Research/courses.html
+++ b/Research/courses.html
@@ -97,3 +97,28 @@
   alt="Picture of the Concrete Semantics book"
   img_class="p-white"
 %}
+{% include feature.html
+  right=true
+  up=true
+  h2="Advanced Topics in Formal Methods and Programming Languages (COMP4011/8011)"
+  text="
+  <p>
+    <strong>Software Verification using Proof Assistants</strong>
+  </p>
+  <p>
+    This course is about mechanical proof assistants, how they work, and what
+    they can be used for. It presents specification and proof techniques used in
+    industrial grade interactive theorem provers (Isabelle/HOL), teaches the
+    theoretical background to the techniques involved, and shows how to use a
+    theorem prover to conduct formal proofs in practice. Topics include higher
+    order logic, natural deduction, lambda calculus, term rewriting, data types
+    and recursive functions, induction principles, and proofs about programs.
+    The course will provide hands-on experience with the proof assistant
+    Isabelle/HOL, which is used in the verification of seL4.
+   </p>"
+  link="https://programsandcourses.anu.edu.au/2026/course/COMP4011/Second%20Semester/9011"
+  button=button
+  img="/Foundation/Membership/LOGOS/anu.svg"
+  alt="ANU School of Computing logo"
+  img_class="p-white"
+%}
\ No newline at end of file