diff --git a/resume.html b/resume.html
index f873fd1..5bfb955 100644
--- a/resume.html
+++ b/resume.html
@@ -45,6 +45,13 @@
             <section>
                 <h1>Projects</h1>
                 <div class="section-content">
+                    <div class="project-container">
+                        <a class="project-link" href="https://dev.danilafe.com/DanilaFe/agda-spa">
+                            <h2>agda-spa</h2>
+                            <i data-feather="link" class="project-link-icon"></i>
+                        </a> &mdash;
+                        Framework for formally-verified lattice-based program analysis in Agda, explained in-depth in <a href="https://danilafe.com/series/static-program-analysis-in-agda/">a series of posts</a>.
+                    </div>
                     <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/abcs">
@@ -85,6 +92,7 @@
                         Compiler from a small imperative language into CHIP-8 bytecode.
                     </div>
                     -->
+                    <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/pegasus">
                             <h2>pegasus</h2>
@@ -92,6 +100,7 @@
                         </a> &mdash;
                         LALR parser generator currently supporting the C and Crystal languages.
                     </div>
+                    -->
                     <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/Scylla">