SanDisk sponsored senior capstone
Acetone Agents
AI-ACETONE explores how TLA+, TLC, and agentic AI can convert model-checker counterexamples into practical test objectives for storage-product validation.
Project brief
Closing test holes before a physical product exists.
Directed testing asks engineers to target specific features and requirement properties. The AI-ACETONE concept uses the exhaustive state exploration of TLC to expose behavior that a test engineer may not have anticipated manually.
The proposed workflow negates selected expectations in a TLA+ specification, lets TLC produce a shortest counterexample trace, and translates that trace into a portable test objective that can support SanDisk validation planning.
Workflow
From formal expectation to test objective.
Select any node in the diagram to see what happens at that stage of the AI-ACETONE process.
What reviewers can inspect
Core project signals.
Reviewers can quickly connect sponsor context, formal-methods terminology, and the people responsible for the work.
Formal-methods foundation
The project brief centers on TLA+, PlusCal, and TLC as the formal specification and model-checking environment for generating useful counterexamples.
Counterexample-driven testing
The capstone centers on turning counterexample traces into actionable test objectives that can help expose intricate design corner cases.
Team
Acetone Agents project team.
Tanmay, Samuel, and Isidro cover sponsor communication, project coordination, workflow support, and implementation.
Tanmay Ghate
Managed key deliverables, supported workflow planning, and served as the main communication bridge between the team and SanDisk sponsor Chris Ortiz.
Samuel Butler
Team lead responsible for project coordination, planning support, and keeping implementation work moving across the group.
Isidro Marquez
Focused on coding the front-end capstone website, building the interactive experience, and polishing the site for review.
Archive focus
Spring 2026 project archive.
This page gathers the project summary, interactive workflow, team roles, and capstone context for review.