Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

University of Virginia
Software Logic
Intellectual Control, Assurance, and Accountability
in the Era of Agentic Software Engineering and Autoformalized Mathematics
Kevin Sullivan
Department of Computer Science
CS6501-010 · Fall 2026
theorem correct : ∀ n, f n = spec n := by decide
Semper crescens · Commit dc651cf