P2P2P Project |

PlusCal to PlantUML to PDF

Automated Documentation Generation

Welcome to the official showcase of P2P2P. Our project automates documentation generation directly from formally verified PlusCal specifications. By bridging the gap between mathematical verification and professional diagramming, we eliminate manual errors and save valuable engineering time.

Project Sponsor

SanDisk

Chris Ortiz - Senior Technologist, Tools & Infrastructure

Rex Jackson - Vice President, Tools & Infrastructure

Technical Advisor

Ogonna Eli

Faculty Mentor - Northern Arizona University

Team

Blueprint Jacks

Jackson Belzer, Christian Lamb, Juan José Serrano Mora, Alejandro Benito Marcos

Project Progress 100%

Meet Our Team

Juan José Serrano
Juan José Serrano Mora
Architect
Backend Rust Pipeline AST Parsing
Alejandro Benito
Alejandro Benito
Release Manager
Documentation Diagrams System Design
Jackson Belzer
Jackson Belzer
Team Lead
Backend Rust Pipeline VSCode
Christian Lamb
Christian Lamb
Recorder
VSCode TypeScript User Workflow

Meet Our Supervisors

Chris Ortiz
Chris Ortiz
Supervisor
Tools & Infrastructure SanDisk
Alejandro Benito
Rex Jackson
Industry Sponsor
Senior Technologist SanDisk
O
Ogonna
University Supervisor & Academic Mentor
Academic Supervision Project Guidance Northern Arizona University

Requirements & Schedule

Major Requirements

Automated diagram generation (Activity, Sequence, State), VSCode integration, Verification-first approach (TLC Enforcement), and Professional PDF output with Hashing/Provenance.

Milestones

Alpha Demo I: Verified Activity Diagram Generation, VSCode Extension, TLC Enforcement.
Alpha Demo II: Sequence & State Diagrams, Improved Readability, PDF Verification.
Acceptance Demo: Template-driven PDFs, auto descriptions, performance optimizations.

Status

All milestones successfully completed and delivered to SanDisk.

The Problem & Solution

The Pains

Currently, formal methods like TLA+ and PlusCal are powerful but hard to communicate. Engineers write code, stakeholders need visuals, and formal models sit in between. Manual diagram generation is slow, quickly outdated, and error-prone. This creates a risk of hidden errors where documentation doesn't match the verified logic.

The Gains

P2P2P provides 100% accurate diagrams consistent with mathematical verification. We save engineers valuable time and effort, ensure determinism (outputs generate in under 60 seconds), and encourage wider adoption of formal methods by making them social and visually accessible.

Project Pitch

Watch Pitch on YouTube

The Product

Value Proposition: "Making formal methods explainable." Automatically generate trusted, professional documentation directly from verified PlusCal models.

Architecture

Modular monolith utilizing a Pipeline Dependency Model (VSCode -> TLC -> Rust -> PlantUML -> LaTeX).

Technologies

VSCode Extension (TypeScript), Rust Backend (Parser/AST), TLA+/TLC Toolchain, PlantUML, LaTeX.

Value Proposition

"Making formal methods explainable." P2P2P automates the generation of trusted, professional documentation directly from verified PlusCal models, bridging the gap between rigorous formal verification and clear stakeholder communication.

Use Case: The Verified Design Cycle

Imagine a firmware engineer designing a new memory controller protocol. traditionally, they would write a specification and then manually draw diagrams—a process prone to errors and desynchronization. With P2P2P, the engineer writes the PlusCal algorithm, verifies it with TLC, and instantly generates a PlantUML sequence diagram and a professional PDF report that are guaranteed to match the verified code.

Codebase

View Repository

Product Demo

Final UGRADS Presentation

Watch Demo on YouTube

Document Archive

Software Design Document

System blueprints, architecture, component interfaces, and pipeline model details.

Download

Software Testing Plan

Unit testing strategy for the Rust backend, integration scenarios, and usability testing.

Download

Final Report

Comprehensive summary of the P2P2P system, development timeline, and future work.

Download

P2P2P User Manual

Installation guide, configuration settings, and daily operation workflow for engineers.

Download

Presentations (Alpha & Acceptance)

Slide decks tracking the project's evolution and milestones demonstrations.

UGRADS Acceptance

Key Achievement: ETAPS 2026

Our team was invited to present the P2P2P project outcomes at the TLA+ Community Event @ ETAPS 2026. This international recognition highlights the innovation and industrial relevance of our work.

Watch on YouTube Download Slides

Get In Touch

Contact Emails js5992@nau.edu, cjl525@nau.edu,
jsb536@nau.edu, ab5637@nau.edu
University Northern Arizona University
Industry Partner SanDisk Corporation