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.

Sponsor SanDisk Tools and Infrastructure
Core method TLA+ specifications and TLC traces
Output Directed software test objectives
Team Three NAU computer science students

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.

TLA+ TLC PlusCal VS Code Rust or Python

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.

Temporal logic State space Counterexample trace

Counterexample-driven testing

The capstone centers on turning counterexample traces into actionable test objectives that can help expose intricate design corner cases.

Property negation Trace reading Test objective

Team

Acetone Agents project team.

Tanmay, Samuel, and Isidro cover sponsor communication, project coordination, workflow support, and implementation.

Tanmay Ghate headshot
Sponsor liaison

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 headshot
Team lead

Samuel Butler

Team lead responsible for project coordination, planning support, and keeping implementation work moving across the group.

Isidro Marquez headshot
Coding and front end

Isidro Marquez

Focused on coding the front-end capstone website, building the interactive experience, and polishing the site for review.

Acetone Agents logo

Archive focus

Spring 2026 project archive.

This page gathers the project summary, interactive workflow, team roles, and capstone context for review.