A PLT Redex formalization of the Verse Calculus, the core calculus for functional logic programming from The Verse Calculus: a Core Calculus for Deterministic Functional Logic Programming. It defines the grammar, evaluation contexts, and rewrite rules.