CS486C Senior Capstone Project

LeGIT/AI

Logical expression Generator Intended for TLA+ with Artificial Intelligence

Transforming natural language requirements into formally verified TLA+ specifications using the power of AI and automated model checking.

Learn More Meet the Team
spec.tla 
VARIABLES state, queue

Init ==
    /\ state = "idle"
    /\ queue = <<>>

Next ==
    \/ (* Process request *)
       /\ state = "idle"
       /\ state' = "processing"
    \/ (* Complete *)
       /\ state = "processing"
       /\ state' = "idle"

About the Project

Bridging the gap between requirements and formal verification

At SanDisk, quality is paramount. To enhance design assurance, this initiative formally specifies designs using PlusCal and TLA+ (Temporal Logic of Actions), enabling rigorous formal verification through model checking.

LeGIT/AI automates the challenging process of converting informal natural language requirements (from NVMe and PCIe specifications) into mathematically rigorous TLA+ formal specifications that can be verified by the TLC model checker.

Technology Stack

Rust TLA+ PlusCal VS Code GitHub Copilot TLC Model Checker
📄
Input PDF Specs
🤖
Processing AI Agent
✓
Output Verified TLA+

Key Features

Streamlining formal specification development

📑

PDF Parsing

Extract requirements context from NVMe and PCIe standard specification documents automatically.

🧠

AI-Powered Generation

Leverage GitHub Copilot Agent Mode to generate TLA+ definitions and formulas from natural language.

✏️

VS Code Integration

Seamlessly edit and refine generated TLA+ specifications within the familiar VS Code IDE.

🔄

Iterative Verification

Automatically verify drafts with TLC model checker for immediate feedback on inconsistencies.

📚

Dictionary Building

Build a global dictionary of VARIABLES and CONSTANTS for consistent cross-specification references.

✅

Formal Verification

Produce exhaustively model-checked TLA+ specifications ensuring correctness across all scenarios.

How It Works

From requirements to verified specifications

1

Input Requirements

Load NVMe/PCIe specification PDFs

→
2

AI Extraction

Extract feature context via AI Agent

→
3

Generate TLA+

Create specification drafts & CFG files

→
4

Verify & Iterate

Model check and refine until verified

Meet the Team

The minds behind LegitCode

Aryan Sharma

Aryan Sharma

Team Member

Northern Arizona University

Gordon Wray

Gordon Wray

Team Member

Northern Arizona University

Brodric Martinez

Brodric Martinez

Team Member

Northern Arizona University

Project Sponsors

Industry partnership with SanDisk Corporation

About TLA+

TLA+ was invented by Leslie Lamport, ACM Turing Award recipient. It is used by major companies including AWS, Microsoft, Oracle, Google, LinkedIn, MongoDB, Intel, ARM, Nvidia, and many more for formal verification of distributed systems.

TLA+ Home GitHub Foundation

Documents

Project resources and presentations

🎥

Elevator Pitch

Watch our elevator pitch presentation on YouTube.

Watch on YouTube
📄

Technological Feasibility Document

Our full technological feasibility analysis for LeGIT/AI.

View Document
📄

Requirements

Coming soon.

Upload pending