Brown's Z3-Peat CS assignment lets students use Claude Code

Brown University's CSCI 0190, running in Fall 2026, has shipped an assignment it calls Z3-Peat. Students redo three earlier problems using the Z3 constraint solver via the pyret-z3 library: a lab-seating solver (LabAssign), a minimum spanning tree (mst-z3), and a course-requirements checker. Two of the researchers we track in our Who's Who directory posted the page.

The flow starts with a hand-encoded warm-up: a system of simultaneous equations and a logic puzzle. "Pick out a logic puzzle to encode using Booleans. If you're lost for one, think about a Sudoku board or, more specifically, a Latin square," the write-up tells students. They then port LabAssign, build mst-z3 (with the key hint that every parent is "strictly closer to the root than its child, for some notion of 'closer' that you make the solver assign"), redo requirement-matching, and submit four Pyret files plus a one-to-two-page PDF analysis.

The permission around Claude is explicit, not grudging. "You are welcome to use Claude Code for this assignment. Indeed, you may find it daunting to do it by hand, whereas with Claude you can do the various experiments above relatively easily," the page says. The reflection it demands cuts the other way: "For each of the three problems, which was easier to write, the solver version or the original, and why? Where did the work go: did the solver remove it, or did it move it?"