Live archive site • Spring 2026

Acetone Agents: AI-ACETONE Capstone Website

Sponsored by SanDisk, this project focuses on generating practical test objectives from model-checker counterexamples using TLA+, TLC, and an AI-assisted workflow.

Open Project Documents GitHub Repository

3Team Members

4Docs Uploaded

SanDiskProject Sponsor

AI-ACETONEProject Track

Project Focus

The team is building a pipeline that starts from formal properties in a TLA+ specification, negates selected expectations, runs TLC, and converts resulting counterexample traces into directed, actionable software test objectives.

This archive site tracks deliverables, team updates, and implementation artifacts throughout the semester.

Architecture Snapshot

1. Parse TLA+ model and property set
2. Generate candidate negations for critical properties
3. Run TLC checks and capture traces
4. Map traces into structured test objectives
5. Track outcomes and refinements in iteration reports

Team

Tanmay Ghate

Formal methods and model workflow support

Samuel Butler

Systems implementation and tooling integration

Isidro Marquez

Project coordination, deliverables, and website management

Document Library

SanDisk ACETONE Project Brief

PDF

Core sponsor-facing description of the AI-ACETONE capstone concept and technical intent.

Open Document

Team Task Tracker

PDF

Active work breakdown and ownership tracking used by the team during implementation.

Open Document

Mayo FTSCS 2015 Reference Paper

PDF

Research foundation used for refinement and out-of-nominal safety methodology context.

Open Paper

CS440 Prototype Report (Project 1)

PDF

Initial proof-of-concept report showing modeling, architecture, and early prototype details.

Open Report

Roadmap

Phase 1: Site FoundationComplete: archival site structure, team identity, doc library.
Phase 2: Core Prototype IntegrationIn progress: pipeline outputs, trace parsing artifacts, and generated objectives.
Phase 3: Architecture + UML UpdatesPlanned: maintain up-to-date diagrams and rationale as architecture evolves.
Phase 4: Final Capstone ArchivePlanned: final demo links, validation evidence, polished documentation.

What This Site Now Includes

Team profile section with photosAll three members represented with visual cards.
Deliverable document hubDirect links to active project PDFs for reviewers and recruiters.
Repository referenceLive codebase link for implementation review.
Mobile-ready designResponsive layout that works for desktop and phone views.