Classical realizability is a rewrite of Kleene's realizability in order to make it compatible with classical reasoning, following the discovery by T. Griffin of a connection between classical reasoning and control operators. J.-L. Krivine used classical realizability semantics to construct novel models of standard set theory (ZF).

I will explain how classical realizability semantics work, how to construct classical realizability models of ZF, and how they differ from forcing models. Notably, each classical realizability model contains a characteristic boolean algebra ∇2, of mysterious structure and weird cardinality. Specifically, I will focus on the model of threads, which showcases these differences.