Models of the Kock-Lawvere axioms 
What are your favorite models of the KL-axioms?

The  motivation is having some basic models to understand the axiom scheme as presented e.g. in Synthetic Geometry of Manifolds by Kock.
In that text he references his other text, Synthetic Differential Geometry, as well as two other sources for models -- the examples in the above text are forgetful functors from categories of rings to the category of sets, and these are cool, but I was wondering if any other 'standard' models have cropped up in the past decade. Any pointers are appreciated.
 A: Here is what I once worked out; I think I remember seeing this published somewhere too but I forget where.
Most of the interesting Kock-Lawvere algebra can be captured in a ring:
$$R_1= \mathbb{R}[t_1,t_2,\dots]/(t_1^2,t_2^2,\dots)$$
For example, this satisfies the principle that only zero can annihilate all infinitesimals:
$$(\forall c\in R)\big[(\forall d \in R)(d^2=0\to cd=0)\to c=0\big]$$
Most of the interesting Kock-Lawvere logic can be captured in a Kripke model based on this, in the sense of intuitionist logic. The Kripke model’s first stage is $R_1$ as above, the second stage is $R_2$ as the image of $R_1$ under the map $t_1\to 0$, the third stage is $R_3$ as the image of $R_2$ under the map $t_2\to 0$, etc.
For example, this satisfies various principles that infinitesimals are in a neighborhood of zero:
$$(\forall d \in R)(d^2=0\to \neg\neg d=0)$$
$$\neg(\forall d \in R)(d^2=0\to d=0)$$
$$(\forall x \in R)\neg(\forall y \in R)(\neg \neg x=y \to x=y)$$
The last of these, which I call the fuzziness of identity, is interesting as a logical statement which follows from the Kock-Lawvere axioms and contradicts classical logic.
Most of the interesting Kock-Lawvere
analysis can be captured in a second-order Henkin model based on this, where the functions from $R$ to $R$ are identified with the smooth functions from $\mathbb{R}$ to $\mathbb{R}$, and $f(r)$ is interpreted as the result of taking the standard part of $r$ (the image of $r$ in $\mathbb{R}$ under the map sending all $t_i$ to 0), taking the power series of $f$ around that standard part, and applying that power series to $r$. E.g., under this interpretation, $\cos(t_1+t_2)= 1-(t_1+t_2)^2/2$, and no more terms are needed since they would all vanish.
For example, this satisfies the central axiom of microlinearity:
$$(\forall f\in R^R)(\exists c\in R)(\forall d \in R)(d^2=0\to f(d)=f(0)+cd)$$
The basic model can also be extended to interpret the order $x<y$ as equivalent to the standard part of $x$ being less than the standard part of $y$. For instance, this falsifies trichotomy but satisfies $(x>0)\vee (x<1)$. The axioms for the other order $x\le y$ are more awkward to fit with these models.
These models are limited, but they are simpler than the topos models, they are accurate enough that they helped me find and correct a minor error in Moerdijk and Reyes’s admirably clear presentation of the axioms, and they may help you understand the Kock-Lawvere axioms better, as they did for me.
