Background

SanDisk is serious about the quality of their popular storage products and strives to be best-in-class in upholding their global brand. The company has moved toward formal verification using TLA+ to catch subtle bugs that traditional review processes miss.

Technical Requirements

• Parse and analyze PlusCal pseudo code specifications
• Generate PlantUML sequence diagrams from PlusCal algorithms
• Generate PlantUML activity diagrams showing system flow
• Integrate with TLA+ model checker for verification
• Produce locked PDF documents with LaTeX formatting
• Ensure synchronization between PlusCal source and generated diagrams

Deliverables

• Complete and well-commented codebase
• Detailed documentation and reference manual
• GitHub repository with development history
• Professional literature for SanDisk product teams

Academic Significance

This project exposes students to cutting-edge formal methods invented by Leslie Lamport (ACM Turing Award winner), used by major companies like AWS, Microsoft, Oracle, Google, LinkedIn, MongoDB, and others.