diff --git a/content/blog/04_spa_agda_fixedpoint.md b/content/blog/04_spa_agda_fixedpoint.md
index b12fc5b..367c695 100644
--- a/content/blog/04_spa_agda_fixedpoint.md
+++ b/content/blog/04_spa_agda_fixedpoint.md
@@ -55,6 +55,7 @@ Now, let's start with the least element of our lattice, denoted \(\bot\).
 A lattice of finite height is guaranteed to have such an element. If it didn't,
 we could always extend chains by tacking on a smaller element to their bottom,
 and then the lattice wouldn't have a finite height anymore.
+{#start-least}
 
 Now, apply \(f\) to \(\bot\) to get \(f(\bot)\). Since \(\bot\) is the least
 element, it must be true that \(\bot \le f(\bot)\). Now, if it's "less than or equal",
diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md
index b08ee5e..e4efcd6 100644
--- a/content/blog/05_spa_agda_semantics/index.md
+++ b/content/blog/05_spa_agda_semantics/index.md
@@ -262,6 +262,7 @@ expressions, and the letter \(v\) to stand for values. Finally, we'll write
 \(\rho, e \Downarrow v\) to say that "in an environment \(\rho\), expression \(e\)
 evaluates to value \(v\)". Our two previous examples of evaluating `x+1` can
 thus be written as follows:
+{#notation-for-environments}
 
 {{< latex >}}
 \{ \texttt{x} \mapsto 42 \}, \texttt{x}+1 \Downarrow 43 \\
diff --git a/content/blog/08_spa_agda_forward/index.md b/content/blog/08_spa_agda_forward/index.md
index b2bb42b..72ad90f 100644
--- a/content/blog/08_spa_agda_forward/index.md
+++ b/content/blog/08_spa_agda_forward/index.md
@@ -10,7 +10,21 @@ draft: true
 In the previous post, I showed that the Control Flow graphs we built of our
 programs match how they are really executed. This means that we can rely
 on these graphs to compute program information. In this post, we finally
-get to compute that information. Let's jump right into it!
+get to compute that information. Here's a quick bit paraphrasing from last time
+that provides a summary of our approach:
+
+1. We will construct a finite-height lattice. Every single element of this
+   lattice will contain information about each variable at each node in the
+   Control Flow Graph.
+2. We will then define a monotonic function that update this information using
+   the structure encoded in the CFG’s edges and nodes.
+3. Then, using the fixed-point algorithm, we will find the least element of the
+   lattice, which will give us a precise description of all program variables at
+   all points in the program.
+4. Because we have just validated our CFGs to be faithful to the language’s
+   semantics, we’ll be able to prove that our algorithm produces accurate results.
+
+Let's jump right into it!
 
 ### Choosing a Lattice
 A lot of this time, we have been [talking about lattices]({{< relref "01_spa_agda_lattices" >}}),
@@ -59,6 +73,7 @@ split our programs into sequences of statements that are guaranteed to execute
 together --- basic blocks. For our analysis, we'll keep per-variable for
 each basic block in the program. Since basic blocks are nodes in the Control Flow
 Graph of our program, our whole lattice will be as follows:
+{#whole-lattice}
 
 {{< latex >}}
 \text{Info} \triangleq \text{NodeId} \to (\text{Variable} \to \text{Sign})
@@ -112,6 +127,7 @@ exact values of `x`, `y`, and `z`, leaving only their signs). The exact details
 of how this partial evaluation is done are analysis-specific; in general, we
 simply require an analysis to provide an evaluator. We will define
 [an evaluator for the sign lattice below](#instantiating-with-the-sign-lattice).
+{#general-evaluator}
 
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 166 167 >}}
 
@@ -136,6 +152,7 @@ current block. Early on, we saw that [the \((\sqcup)\) operator models disjuncti
 \((\sqcup)\) to the variable-sign maps of all predecessors. The
 [reference _Static Program Analysis_ text](https://cs.au.dk/~amoeller/spa/)
 calls this operation \(\text{JOIN}\):
+{#join-preds}
 
 {{< latex >}}
 \textit{JOIN}(v) = \bigsqcup_{w \in \textit{pred}(v)} \llbracket w \rrbracket
@@ -272,6 +289,7 @@ Actually, we haven't yet seen that `updateVariablesFromStmt`. This is
 a function that we can define using the user-provided abtract interpretation
 `eval`. Specifically, it handles the job of updating the sign of a variable
 once it has been assigned to (or doing nothing if the statement is a no-op).
+{#define-updateVariablesFromStmt}
 
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 191 193 >}}
 
diff --git a/content/blog/09_spa_agda_verified_forward/index.md b/content/blog/09_spa_agda_verified_forward/index.md
new file mode 100644
index 0000000..74c1db0
--- /dev/null
+++ b/content/blog/09_spa_agda_verified_forward/index.md
@@ -0,0 +1,548 @@
+---
+title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 9: Verifying the Forward Analysis"
+series: "Static Program Analysis in Agda"
+description: "In this post, I prove that the sign analysis from the previous is correct"
+date: 2024-12-17T19:51:00-08:00
+tags: ["Agda", "Programming Languages"]
+draft: true
+left_align_code: true
+---
+
+In the previous post, we put together a number of powerful pieces of machinery
+to construct a sign analysis. However, we still haven't verified that this
+analysis produces correct results. For the most part, we already have the
+tools required to demonstrate correctness; the most important one
+is the [validity of our CFGs]({{< relref "07_spa_agda_semantics_and_cfg" >}})
+relative to [the semantics of the little language]({{< relref "05_spa_agda_semantics" >}}).
+
+### High-Level Algorithm
+We'll keep working with the sign lattice as an example, keeping in mind
+how what we do generalizes to a any lattice \(L\) describing a variable's
+state. The general shape of our argument will be as follows, where I've underlined and
+numbered assumptions or aspects that we have yet to provide.
+
+1. Our fixed-point analysis from the previous section gave us a result \(r\)
+   that satisfies the following equation:
+
+   {{< latex >}}
+   r = \text{update}(\text{join}(r))
+   {{< /latex >}}
+
+   Above \(\text{join}\) applies the [predecessor-combining function]({{< relref "08_spa_agda_forward#join-preds" >}})
+   from the previous post to each state (corresponding to `joinAll` in Agda)
+   and \(\text{update}\) performs one round of abstract interpretation.
+
+2. Because of the [correspondence of our semantics and CFGs]({{< relref "07_spa_agda_semantics_and_cfg" >}}),
+   each program evaluation in the form \(\rho, s \Rightarrow \rho'\)
+   corresponds to a path through the Control Flow Graph. Along the path,
+   each node contains simple statements, which correspond to intermediate steps
+   in evaluating the program. These will also be in the form
+   \(\rho_1, b \Rightarrow \rho_2\).
+
+3. We will proceed iteratively, stepping through the trace one basic block at
+   a time. At each node in the graph:
+   * We will assume that the beginning state (the variables in \(\rho_1\)) are
+     {{< internal "correctly-described" >}}
+     correctly described
+     {{< /internal >}}
+     by one of the predecessors of the current node. Since
+     {{< internal "disjunction" >}}
+     joining represents "or"
+     {{< /internal >}},
+     that is the same
+     as saying that \(\text{join}(r)\)
+     contains an accurate description of \(\rho_1\).
+
+   * Because
+     {{< internal "abstract-interpretation" >}}
+     the abstract interpretation function preserves accurate descriptions
+     {{< /internal >}},
+     if \(\text{join}(r)\) contains an accurate description \(\rho_1\), then applying our
+     abstract interpretation function via \(\text{update}\) should result in
+     a map that contains an accurate-described \(\rho_2\). In other words, \(\text{update}(\text{join}(r))\)
+     describes \(\rho_2\) at the current block.
+     {{< internal "equivalence" >}}
+     By the equation above
+     {{< /internal >}}, that's the same as saying
+     \(r\) describes \(\rho_2\) at the current block.
+
+   * Since the trace is a path through a graph, there must be an edge from
+     the current basic block to the next. This means that the current basic
+     block is a predecessor of the next one. From the previous point, we know
+     that \(\rho_2\) is accurately described by this predecessor, fulfilling
+     our earlier assumption and allowing us to continue iteration.
+
+So, what are the missing pieces?
+
+1. We need to define what it means for a lattice (like our sign lattice)
+   to "correctly describe" what happens when evaluating a program for real.
+   For example, the \(+\) in sign analysis describes values that are bigger than zero,
+   and a map like `{x:+}` states that `x` can only take on positive values.
+2. We've seen before [the \((\sqcup)\) operator models disjunction
+   ("A or B")]({{< relref "01_spa_agda_lattices#lub-glub-or-and" >}}), but
+   that was only an informal observation; we'll need to specify it preceisely.
+3. Each analysis [provides an abstract interpretation `eval` function]({{< relref "08_spa_agda_forward#general-evaluator" >}}).
+   However, until now, nothing has formally constrained this function; we could
+   return \(+\) in every case, even though that would not be accurate. We will
+   need, for each analysis, a proof that its `eval` preserves accurate descriptions.
+4. The equalities between our lattice elements [are actually equivalences]({{< relref "01_spa_agda_lattices#definitional-equality" >}}),
+   which helps us use simpler representations of data structures. Thus, even
+   in statements of the fixed point algorithm, our final result is a value \(a\)
+   such that \(a \approx f(a)\). We need to prove that our notion of equivalent
+   lattice elements plays nicely with correctness.
+
+Let's start with the first bullet point.
+
+### A Formal Definition of Correctness
+
+When a variable is mapped to a particular sign (like `{ "x": + }`),
+what that really says is that the value of `x` is greater than zero. Recalling
+from [the post about our language's semantics]({{< relref "05_spa_agda_semantics#notation-for-environments" >}})
+that we use the symbol \(\rho\) to represent mappings of variables to
+their values, we might write this claim as:
+
+{{< latex >}}
+\rho(\texttt{x}) > 0
+{{< /latex >}}
+
+This is a good start, but it's a little awkward defining the meaning of "plus"
+by referring to the context in which it's used (the `{ "x": ... }` portion
+of the expression above). Instead, let's associate with each sign (like \(+\)) a
+predicate: a function that takes a value, and makes a claim about that value
+("this is positive"):
+
+{{< latex >}}
+\llbracket + \rrbracket\ v = v > 0
+{{< /latex >}}
+
+The notation above is a little weird unless you, like me, have a background in
+Programming Language Theory (❤️). This comes from [denotational semantics](https://en.wikipedia.org/wiki/Denotational_semantics);
+generally, one writes:
+
+{{< latex >}}
+\llbracket \text{thing} \rrbracket = \text{the meaning of the thing}
+{{< /latex >}}
+
+Where \(\llbracket \cdot \rrbracket\) is really a function (we call it
+the _semantic function_) that maps things to
+their meaning. Then, the above equation is similar to the more familiar
+\(f(x) = x+1\): function and arguments on the left, definition on the right. When
+the "meaning of the thing" is itself a function, we could write it explicitly
+using lambda-notation:
+
+{{< latex >}}
+\llbracket \text{thing} \rrbracket = \lambda x.\ \text{body of the function}
+{{< /latex >}}
+
+Or, we could use the Haskell style and write the new variable on the left of
+the equality:
+
+{{< latex >}}
+\llbracket \text{thing} \rrbracket\ x = \text{body of the function}
+{{< /latex >}}
+
+That is precisely what I'm doing above with \(\llbracket + \rrbracket\).
+With this in mind, we could define the entire semantic function for the
+sign lattice as follows:
+
+{{< latex >}}
+\llbracket + \rrbracket\ v = v\ \texttt{>}\ 0 \\
+\llbracket 0 \rrbracket\ v = v\ \texttt{=}\ 0 \\
+\llbracket - \rrbracket\ v = v\ \texttt{<}\ 0 \\
+\llbracket \top \rrbracket\ v = \text{true} \\
+\llbracket \bot \rrbracket\ v = \text{false}
+{{< /latex >}}
+
+In Agda, the integer type already distinguishes between "negative natural" or
+"positive natural" cases, which made it possible to define the semantic function
+{{< sidenote "right" "without-note" "without using inequalities." >}}
+Reasoning about inequalities is painful, sometimes requiring a number of
+lemmas to arrive at a result that is intuitively obvious. Coq has a powerful
+tactic called <a href="https://coq.inria.fr/doc/v8.11/refman/addendum/micromega.html#coq:tacn.lia"><code>lia</code></a>
+that automatically solves systems of inequalities, and I use it liberally.
+However, lacking such a tactic in Agda, I would like to avoid inequalities
+if they are not needed.
+{{< /sidenote >}}
+
+{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 114 119 >}}
+
+Notably, \(\llbracket \top \rrbracket\ v\) always holds, and
+\(\llbracket \bot \rrbracket\ v\) never does. __In general__, we will always
+need to define a semantic function for whatever lattice we are choosing for
+our analysis.
+
+It's important to remember from the previous post that the sign lattice
+(or, more generally, our lattice \(L\)) is only a component of the
+[lattice we use to instantiate the analysis]({{< relref "08_spa_agda_forward#whole-lattice" >}}).
+We at least need to define what it means for the \(\text{Variable} \to \text{Sign}\)
+portion of that lattice to be correct. This way, we'll have correctness
+criteria for each key (CFG node) in the top-level \(\text{Info}\) lattice.
+Since a map from variables to their sign characterizes not a single value \(v\)
+but a whole environment \(\rho\), something like this is a good start:
+
+{{< latex >}}
+\llbracket \texttt{\{} x_1: s_1, ..., x_n: s_n \texttt{\}} \rrbracket\ \rho = \llbracket s_1 \rrbracket\ \rho(x_1)\ \text{and}\ ...\ \text{and}\ \llbracket s_n \rrbracket\ \rho(x_n)
+{{< /latex >}}
+
+As a concrete example, we might get:
+
+{{< latex >}}
+\llbracket \texttt{\{} \texttt{x}: +, \texttt{y}: - \texttt{\}} \rrbracket\ \rho = \rho(\texttt{x})\ \texttt{>}\ 0\ \text{and}\ \rho(\texttt{y})\ \texttt{<}\ 0
+{{< /latex >}}
+
+This is pretty good, but not quite right. For instance, the initial state of
+the program --- before running the analysis --- assigns \(\bot\) to each
+element. This is true because our fixed-point algorithm [starts with the least
+element of the lattice]({{< relref "04_spa_agda_fixedpoint#start-least" >}}).
+But even for a single-variable map `{x: ⊥ }`, the semantic function above would
+give:
+
+{{< latex >}}
+\llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \text{false}
+{{< /latex >}}
+
+That's clearly not right: our initial state should be possible, lest
+the entire proof be just a convoluted [_ex falso_](https://en.wikipedia.org/wiki/Principle_of_explosion)!
+
+There is another tricky aspect of our analysis, which is primarily defined
+[using the join (\(\sqcup\)) operator]({{< relref "08_spa_agda_forward#join-preds" >}}).
+Observe the following example:
+
+```C
+// initial state: { x: ⊥ }
+if b {
+  x = 1; // state: { x: + }
+} else {
+  // state unchanged: { x: ⊥ }
+}
+// state: { x: + } ⊔ { x: ⊥ } = { x: + }
+```
+
+Notice that in the final state, the sign of `x` is `+`, even though when
+`b` is `false`, the variable is never set. In a simple language like ours,
+without variable declaration points, this is probably the best we could hope
+for. The crucial observation, though, is that the oddness only comes into
+play with variables that are not set. In the "initial state" case, none
+of the variables have been modified; in the `else` case of the conditional,
+`x` was never assigned to. We can thus relax our condition to an if-then:
+if a variable is in our environment \(\rho\), then the variable-sign lattice's
+interpretation accurately describes it.
+
+{{< latex >}}
+\begin{array}{ccc}
+\llbracket \texttt{\{} x_1: s_1, ..., x_n: s_n \texttt{\}} \rrbracket\ \rho & = & & \textbf{if}\ x_1 \in \rho\ \textbf{then}\ \llbracket s_1 \rrbracket\ \rho(x_1)\ \\ & & \text{and} & ... \\ & & \text{and} &  \textbf{if}\ x_n \in \rho\ \textbf{then}\ \llbracket s_n \rrbracket\ \rho(x_n)
+\end{array}
+{{< /latex >}}
+
+The first "weird" case now results in the following:
+
+{{< latex >}}
+\llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \textbf{if}\ \texttt{x} \in \rho\ \textbf{then}\ \text{false}
+{{< /latex >}}
+
+Which is just another way of saying:
+
+{{< latex >}}
+\llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \texttt{x} \notin \rho
+{{< /latex >}}
+
+In the second case, the interpretation also results in a true statement:
+
+{{< latex >}}
+\llbracket \texttt{\{} \texttt{x}: + \texttt{\}} \rrbracket\ \rho = \textbf{if}\ \texttt{x} \in \rho\ \textbf{then}\ \texttt{x} > 0
+{{< /latex >}}
+
+In Agda, I encode the fact that a verified analysis needs a semantic function
+\(\llbracket\cdot\rrbracket\) for its element lattice \(L\) by taking such
+a function as an argument called `⟦_⟧ˡ`:
+
+{{< codelines "Agda" "agda-spa/Analysis/Forward.agda" 246 253 "hl_lines=5" >}}
+
+I then define the semantic function for the variable-sign lattice in the following
+way, which eschews the "..." notation in favor of a more Agda-compatible (and
+equivalent) form:
+
+{{< codelines "Agda" "agda-spa/Analysis/Forward.agda" 255 256 >}}
+
+The above reads roughly as follows:
+
+> For every variable `k` and sign [or, more generally, lattice element] `l` in
+> the variable map lattice, if `k` is in the environment `ρ`, then it satisfies
+> the predicate given by the semantic function applied to `l`.
+
+Let's recap: we have defined a semantic function for our sign lattice, and
+noted that to define a verified analysis, we always need such a semantic function.
+We then showed how to construct a semantic function for a whole variable map
+(of type \(\text{Variable} \to \text{Sign}\), or \(\text{Variable}\to L\)
+in general). We also wrote some Agda code doing all this. As a result, we
+have filled in the missing piece for {{< internalref "correctly-described" >}}property{{< /internalref >}}.
+
+However, the way that we brought in the semantic function in the Agda code
+above hints that there's more to be discussed. What's `latticeInterpretationˡ`?
+In answering that question, we'll provide evidence for
+{{< internalref "disjunction" >}}property{{< /internalref >}}
+and
+{{< internalref "equivalence" >}}property{{< /internalref >}}.
+
+### Properties of the Semantic Function
+
+As we briefly saw earlier, we loosened the notion of equality to that equivalences,
+which made it possible to ignore things like the ordering of key-value pairs
+in maps. That's great and all, but nothing is stopping us from defining semantic functions that violate our equivalence!
+Supposing \(a \approx f(a)\), as far
+as Agda is concerned, even though \(a\) and \(f(a)\) are "equivalent",
+\(\llbracket a \rrbracket\) and \(\llbracket f(a) \rrbracket\) may be
+totally different. For a semantic function to be correct, it must produce
+the same predicate for equivalent elements of lattice \(L\). That's
+{{< internalref "equivalence" >}}missing piece{{< /internalref >}}.
+
+Another property of semantic functions that we will need to formalize
+is that \((\sqcup)\) represents disjunction.
+This comes into play when we reason about the correctness of predecessors in
+a Control Flow Graph. Recall that during the last step of processing a given node,
+when we are trying to move on to the next node in the trace, we have knowledge
+that the current node's variable map accurately describes the intermediate
+environment. In other words, \(\llbracket \textit{vs}_i \rrbracket\ \rho_2\) holds, where
+\(\textit{vs}_i\) is the variable map for the current node. We can generalize this
+kowledge a little, and get:
+
+{{< latex >}}
+\llbracket \textit{vs}_1 \rrbracket\ \rho_2\ \text{or}\ ...\ \text{or}\ \llbracket \textit{vs}_n \rrbracket\ \rho_2
+{{< /latex >}}
+
+However, the assumption that we _need_ to hold when moving on to a new node
+is in terms of \(\textit{JOIN}\), which combines all the predecessors' maps
+\(\textit{vs}_1, ..., \textit{vs}_n\) using \((\sqcup)\). Thus, we will need to be in a world where
+the following claim is true:
+
+{{< latex >}}
+\llbracket \textit{vs}_1 \sqcup ... \sqcup \textit{vs}_n \rrbracket\ \rho
+{{< /latex >}}
+
+To get from one to the other, we will need to rely explicitly on the fact
+that \((\sqcup)\) encodes "or". It's not necessary for the forward analysis,
+but a similar property ought to hold for \((\sqcap)\) and "and". This
+constraint provides {{< internalref "disjunction" >}}missing piece{{< /internalref >}}.
+
+I defined a new data type that bundles a semantic function with proofs of
+the properties in this section; that's precisely what `latticeInterpretationˡ`
+is:
+
+{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 66 73 >}}
+
+In short, to leverage the framework for verified analysis, you would need to
+provide a semantic function that interacts properly with `≈` and `∨`.
+
+### Correctness of the Evaluator
+
+All that's left is {{< internalref "abstract-interpretation" >}}the last missing piece, {{< /internalref >}},
+which requires that `eval` matches the semantics of our language. Recall
+the signature of `eval`:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 166 166 >}}
+
+It operates on expressions and variable maps, which themselves associate a
+sign (or, generally, an element of lattice \(L\)), with each variable. The
+"real" evaluation judgement, on the other hand, is in the form
+\(\rho, e \Downarrow v\), and reads "expression \(e\) in environment \(\rho\)
+evaluates to value \(v\)". In Agda:
+
+{{< codelines "agda" "agda-spa/Language/Semantics.agda" 27 27 >}}
+
+Let's line up the types of `eval` and the judgement. I'll swap the order of arguments
+for `eval` to make the correspondence easier to see:
+
+{{< latex >}}
+\begin{array}{ccccccc}
+\text{eval} & : & (\text{Variable} \to \text{Sign}) & \to & \text{Expr} & \to & \text{Sign} \\
+\cdot,\cdot\Downarrow\cdot & : & (\text{Variable} \to \text{Value}) & \to & \text{Expr} & \to & \text{Value} & \to & \text{Set} \\
+& & \underbrace{\phantom{(\text{Variable} \to \text{Value})}}_{\text{environment-like inputs}} & & & & \underbrace{\phantom{Value}}_{\text{value-like outputs}}
+\end{array}
+{{< /latex >}}
+
+Squinting a little, it's almost like the signature of `eval` is the signature
+for the evaluation judgement, but it forgets a few details (the exact values
+of the variables) in favor of abstractions (their signs). To show that `eval`
+behaves correctly, we'll want to prove that this forgetful correspondence holds.
+
+Concretely, for any expression \(e\), take some environment \(\rho\), and "forget"
+the exact values, getting a sign map \(\textit{vs}\). Now, evaluate the expression
+to some value \(v\) using the semantics, and also, compute the expression's
+expected sign \(s\) using `eval`. The sign should be the same as forgetting
+\(v\)'s exact value. Mathematically,
+
+{{< latex >}}
+\forall e, \rho, v, \textit{vs}.\ \textbf{if}\ \llbracket\textit{vs}\rrbracket \rho\ \text{and}\ \rho, e \Downarrow v\ \textbf{then}\ \llbracket \text{eval}\ \textit{vs}\ e\rrbracket v
+{{< /latex >}}
+
+In Agda:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 286 287 >}}
+
+For a concrete analysis, we need to prove the above claim. In the case of
+sign analysis, this boils down to a rather cumbersome proof by cases. I will collapse
+the proofs to save some space and avoid overwhelming the reader.
+
+{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 237 258 "" "**(Click here to expand the proof of correctness for plus)**" >}}
+{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 261 282 "" "**(Click here to expand the proof of correctness for minus)**" >}}
+
+{{< codelines "agda" "agda-spa/Analysis/Sign.agda" 284 294 "" >}}
+
+This completes {{< internalref "abstract-interpretation" >}}our last missing piece,{{< /internalref >}}.
+All that's left is to put everything together.
+
+### Proving The Analysis Correct
+
+#### Lifting Expression Evaluation Correctness to Statements
+The individual analyses (like the sign analysis) provide only an evaluation
+function for _expressions_, and thus only have to prove correctness of
+that function. However, our language is made up of statements, with judgements
+in the form \(\rho, s \Rightarrow \rho'\). Now that we've shown (or assumed)
+that `eval` behaves correctly when evaluating expressions, we should show
+that this correctness extends to evaluating statements, which in the
+forward analysis implementation is handled by the
+[`updateVariablesFromStmt` function]({{< relref "08_spa_agda_forward#define-updateVariablesFromStmt" >}}).
+
+The property we need to show looks very similar to the property for `eval`:
+
+{{< latex >}}
+\forall b, \rho, \rho', \textit{vs}.\ \textbf{if}\ \llbracket\textit{vs}\rrbracket \rho\ \text{and}\ \rho, b \Rightarrow \rho'\ \textbf{then}\ \llbracket \text{updateVariablesFromStmt}\ \textit{vs}\ b\rrbracket \rho'
+{{< /latex >}}
+
+In Agda:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 291 291 >}}
+
+The proof is straightforward, and relies on the semantics of the [map update]({{< relref "08_spa_agda_forward#generalized-update" >}}).
+Specifically, in the case of an assignment statement \(x \leftarrow e\), all we
+do is store the new sign computed from \(e\) into the map at \(x\). To
+prove the correctness of the entire final environment \(\rho'\), there are
+two cases to consider:
+
+* A variable in question is the newly-updated \(x\). In this case, since
+  `eval` produces correct signs, the variable clearly has the correct sign.
+  This is the first highlighted chunk in the below code.
+* A variable in question is different from \(x\). In this case, its value
+  in the environment \(\rho'\) should be the same as it was prior, and
+  its sign in the updated variable map is the same as it was in the original.
+  Since the original map correctly described the original environment, we know
+  the sign is correct. This is the second highlighted chunk in the below
+  code.
+
+The corresponding Agda proof is as follows:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 291 305 "hl_lines=5-7 10-15" >}}
+
+From this, it follows with relative ease that each basic block in the lattice,
+when evaluated, produces an environment that matches the prediction of our
+forward analysis.
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 318 318 >}}
+
+#### Walking the Trace
+
+Finally, we get to the meat of the proof, which follows the [outline](#high-level-algorithm). First,
+let's take a look at `stepTrace`, which implements the second bullet in
+our iterative procedure. I'll show the code, then we can discuss it
+in detail.
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 324 342 >}}
+
+The first `let`-bound variable, `⟦joinAll-result⟧ρ₁` is kind of an intermediate
+result, which I was forced to introduced because `rewrite` caused Agda to
+allocate ~100GB of memory. It simply makes use of the fact that `joinAll`, the
+function that performs predecessor joining for each node in the CFG, sets
+every key of the map accordingly.
+
+The second `let`-bound variable, `⟦analyze-result⟧`, steps through a given
+node's basic block and leverages our proof of statement-correctness to validate
+that the final environment `ρ₂` matches the predication of the analyzer.
+
+The last two `let`-bound variables apply the equation we wrote above:
+
+{{< latex >}}
+r = \text{update}(\text{join}(r))
+{{< /latex >}}
+
+Recall that `analyze` is the combination of `update` and `join`:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 226 227 >}}
+
+Finally, the `in` portion of the code uses `⟦⟧ᵛ-respects-≈ᵛ`, a proof
+of {{< internalref "equivalence" >}}property{{< /internalref >}}, to produce
+the final claim in terms of the `result` map.
+
+Knowing how to step, we can finally walk the entire trace, implementing
+the iterative process:
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 344 357 >}}
+
+The first step --- assuming that one of the predecessors of the
+current node satisfies the initial environment `ρ₁` --- is captured by
+the presence of the argument `⟦joinForKey-s₁⟧ρ₁`. We expect the calling code
+to provide a proof of that.
+
+The second step, in both cases, is implemented using `stepTrace`,
+as we saw above. That results in a proof that at the end of the current basic
+block, the final environment `ρ₂` is accurately described.
+
+From there, we move on to the third iterative step, if necessary. The
+sub-expression `edge⇒incoming s₁→s₂` validates that, since we have an edge
+from the current node to the next, we are listed as a predecessor. This,
+in turn, means that we are included in the list of states-to-join for the
+\(\textit{JOIN}\) function. That fact is stored in `s₁∈incomingStates`.
+Finally, relying on
+{{< internalref "disjunction" >}}property{{< /internalref >}},
+we construct an assumption fit for a recursive invocation of `walkTrace`,
+and move on to the next CFG node. The `foldr` here is motivated by the fact
+that "summation" using \((\sqcup)\) is a fold.
+
+When the function terminates, what we have is a proof that the final program
+state is accurately described by the results of our program analysis. All
+that's left is to kick off the walk. To do that, observe that the initial state
+has no predecessors (how could it, if it's at the beginning of the program?).
+That, in turn, means that this state maps every variable to the bottom element.
+Such a variable configuration only permits the empty environment \(\rho = \varnothing\).
+If the program evaluation starts in an empty environment, we have the assumption
+needed to kick off the iteration.
+
+{{< codelines "agda" "agda-spa/Analysis/Forward.agda" 359 366 "hl_lines=7" >}}
+
+Take a look at the highlighted line in the above code block in particular.
+It states precisely what we were hoping to see: that, when evaluating
+a program, the final state when it terminates is accurately described by
+the `result` of our static program analysis at the `finalState` in the CFG.
+We have done it!
+
+### Future Work
+
+It took a lot of machinery to get where we are, but there's still lots of
+things to do.
+
+1. __Correctness beyond the final state__: the statement we've arrived at
+   only shows that the final state of the program matches the results of
+   the analysis. In fact, the property hold for all intermediate states, too.
+   The only snag is that it's more difficult to _state_ such a claim.
+
+   To do something like that, we probably need a notion of "incomplete evaluations"
+   of our language, which run our program but stop at some point before the end.
+   A full execution would be a special case of such an "incomplete evaluation"
+   that stops in the final state. Then, we could restate `analyze-correct`
+   in terms of partial evaluations, which would strengthen it.
+2. __A more robust language and evaluation process__: we noted above that
+   our join-based analysis is a little bit weird, particularly in the
+   cases of uninitialized variables. There are ways to adjust our language
+   (e.g., introducing variable declaration points) and analysis functions
+   (e.g., only allowing assignment for declared variables) to reduce
+   the weirdness somewhat. They just lead to a more complicated language.
+3. __A more general correctness condition__: converting lattice elements into
+   predicates on values gets us far. However, some types of analyses make claims
+   about more than the _current_ values of variables. For instance, _live variable
+   analysis_ checks if a variable's current value is going to be used in the
+   future. Such an analysis can help guide register (re)allocation. To
+   talk about future uses of a variable, the predicate will need to be formulated
+   in terms of the entire evaluation proof tree. This opens a whole can
+   of worms that I haven't begun to examine.
+
+Now that I'm done writing up my code so far, I will start exploring these
+various avenues of work. In the meantime, though, thanks for reading!