99P Labs/Honda Research Institute: Network Sandbox

As critical infrastructure comes to rely on digital networks, it becomes ever more important to understand how these networks are impacted by the real world. To learn about and prepare for these impacts, we worked with Honda’s 99P Labs to prototype a network sandbox with support for simulating real world environments.

This prototype leverages Mininet, Grafana, Docker and OpenStreetMaps to simulate tests, network topologies, and wireless communication protocols in a user-friendly, repeatable way. Our work coordinating these technologies, combatting their limitations, and exploring alternative solutions proves the feasibility of the use case and assists 99P Labs in deriving usable insights for building the resilient, performant networks of the future.

Amazon AWS: Building Mathematically-Proven Libraries for the Future of Secure Programming

Dafny is a programming language that allows developers to formally verify their code and catch logical errors before it runs. However, its standard libraries are still missing some of the basic modules that developers rely on every day, such as Statistics and Datetime.

Our project focuses on building verified implementations of common statistical functions, such as mean, median and variance, as well as a complete Datetime library for handling dates, durations, time zones, and formatting.

Each function is mathematically proven to be correct and designed to integrate easily with existing Dafny code. By expanding Dafny with these reliable and reusable components, our work makes it easier for developers to write secure programs and avoid production-level bugs.

Amazon AWS: Differential Testing in Python

Software developers spend countless hours refactoring and optimizing code, but a single mistake during these “safe” changes can introduce bugs that crash production systems.

Our project develops an automated differential testing tool that compares the behavior of two versions of a program across thousands of generated test cases to detect subtle regressions introduced during refactoring or optimization. The tool's codebase is tested entirely on open-source benchmarks and powered by automated type inference. This tool demonstrates how intelligent testing can improve the reliability of Python software development and make progress toward safer, large-scale software maintenance. 

Our toolkit can help engineering teams catch hidden bugs early, reduce manual testing effort, and accelerate release cycles, fundamentally improving the stability and trustworthiness of evolving large codebases.

Amazon AWS: Encoding Typescript Semantics for Efficient Code Reasoning

Software bugs and security vulnerabilities cost businesses millions when discovered in production. Yet existing verification frameworks for Typescript provide limited support for reasoning about its complex semantics. This leaves developers with little visibility into logical or security errors until runtime.

Our solution involved extending support on Strata — a unified platform for formalizing language syntax and semantics — to translate TypeScript code into a format that Strata can analyze. Our work lays the foundation to integrate verification tools into IDEs for the automated detection of errors and vulnerabilities during development. This enables automated detection of errors and vulnerabilities directly during development and integrates verification tools into IDEs like VS Code.

The goal of this project is for developers can identify and resolve critical issues early within their development environment, significantly reducing production risks. Our work strengthens automated code verification for one of the most widely used enterprise programming languages in cloud development.

Amazon AWS: Enhancing Kani’s Data Handling Service

Kani is a verification tool that mathematically proves Rust programs behave correctly. Previously, it presented results only as console text, which made it hard for developers to read, analyze, or integrate results into larger systems. This limitation restrained adoption in continuous integration and DevOps environments, where reproducibility, traceability and data-driven insights are essential.

To solve this problem, we developed a JSON export system that converts Kani's raw verification output into structured, machine-readable data containing full metadata on test cases, verification status, timing, and solver statistics. The new format enables automated data collection, comparison across builds, and integration with visualization tools and analytics dashboards.

When deployed, this enhancement transforms Kani from an independent verification utility into a fully automatable component of modern DevOps workflows, supporting continuous verification, trend tracking and early detection of logical regressions throughout the software lifecycle.

Amazon AWS: Programmatically Verifying AI-Generated API Calls

Developers increasingly rely on AI agents to automate API calls, but large language models (LLMs) sometimes “hallucinate,” generating plausible but incorrect parameters. These errors can lead to data loss, downtime, broken trust, and security breaches.

Our team built the Constraint Finder Tool to avoid LLM-generated API calls that are invalid, insecure or unreliable. The tool automatically generates, corrects and formalizes API constraints based on the documentation and observed API behaviors. The resulting constraints serve as input to the validation tools that check every LLM-generated call before API invocation.

This tool, piloted using AWS APIs, empowers developers to harness AI safely, preventing costly errors, and demonstrating how AI‑driven automation can be made more reliable.

City of San Jose: Operation Silicon Shield

Upcoming major sporting events are expected to bring nearly half a million visitors to the San José metropolitan area. To securely prepare for the increase in the network traffic, the City of San José has tasked our team with conducting simulated cyberattacks (known as penetration testing) on its essential public service networks. These networks encompass the public Wi-Fi infrastructure for the San José Police Department, Emergency Operations Center, and Mineta International Airport.

The primary goal is to proactively identify security weaknesses within these critical systems before they can be exploited by malicious attackers. Our work aims to be conducted in a secure, controlled environment to ensure zero disruption to city operations and availability while also ensuring  that no sensitive data is exposed. The findings will provide city leaders with actionable recommendations to immediately strengthen defenses, thereby protecting public safety and maintaining community trust in essential services.

Clearview Federal Credit Union: Clearshield

According to the Federal Trade Commission (FTC), reports from adults aged 60+ losing $10,000 or more to imposter scams, have increased more than four-fold between 2020 and 2024. This rise highlights a growing vulnerability among older adults and the urgent need for more effective fraud detection and prevention tools.

To help address this issue locally in Pittsburgh, our team is working with Clearview Federal Credit Union on ClearShield, a data-driven fraud prevention approach. The goal is to leverage machine learning, behavioral analytics, and workflow automation designed to detect and flag suspicious transactions in near-real time. The credit union can potentially investigate flagged transactions earlier. This allows them to intervene before losses occur. This initiative aims not only to strengthen financial safety for vulnerable populations, but also to potentially strengthen trust and confidence among credit union members.

CMU Heinz: Cyber SimLab

Our team developed a hands-on cybersecurity simulation designed to bridge the gap between classroom theory and real-world practice. The simulation replicates multiple stages of realistic cyberattacks, including phishing, malware infection, and ransomware. It guides learners through every step of the incident response process, from detection and containment, to analysis and recovery.

Built using open source software and emulated within TopoMojo, the simulation immerses students in authentic enterprise environments where they apply security tools, interpret live data and make critical response decisions. This approach transforms learning into an active experience that mirrors the challenges faced by cybersecurity professionals.

By focusing on practical application rather than theory alone, our project empowers both students and instructors to develop actual operational readiness. The simulation also serves as a prototype for future training scenarios, advancing experiential cybersecurity education across academic and industry settings.

Federal Reserve Bank of St. Louis: FRED GPT - An Agentic System for Exploring Economic Data and Concepts

FRED GPT is an interactive web platform that helps users easily explore and interpret U.S. economic data using plain language conversation. Existing Federal Reserve resources are fragmented across multiple systems, making it difficult to connect data, documents, and historical insights.

To address this, our Practicum team built FRED GPT from the ground up, developing a LangChain-based RAG pipeline with AWS Bedrock and OpenSearch integration. We optimized query understanding, designed interpretable outputs, and built a visualization front end. By making data exploration intuitive and transparent, FRED GPT supports more informed research, teaching and decision-making.

Groq: PyTorch Tracer Caching Optimization

PyTorch is currently the most popular Python library for building deep learning models. Compiling PyTorch models with the new PyTorch 2.0 dynamo compiler can unlock major speedups, but today it could take multiple minutes to compile just once and often fails with cryptic errors. 

Our project builds a linter that statically scans the code in sub-second time, flags patterns that typically break compilation and offers automatic fixes or clear guidance.

With this tool, teams can spend less time debugging and more time training and deploying on modern hardware. We aim to lower the barrier to adopting PyTorch 2.0, reducing costs and accelerating innovation across research and industry.

Itanta Analytics: Database Abstraction Layer Implementation

This project enhances real-time analytics for manufacturing and pharmaceutical clients who rely on dashboards to monitor production. The existing MongoDB backend struggled to process large volumes of time-series data, resulting in query times exceeding several minutes.

To address this, we migrated the backend to QuestDB and built a Python client that mimics MongoDB’s interface, minimizing code changes and enabling dynamic switching between the two databases during migration. The goal is to reduce dashboard latency to under one minute, giving users real-time visibility and a smoother analytics experience.

Post Road Foundation - MTEP Red Teaming

As the power grid evolves toward cleaner, more reliable energy, the Post Road Foundation’s Maine Transactive Energy Pilot (MTEP) is pioneering a smart-grid system that coordinates residential energy resources. A crucial part of their solution is a gateway device that manages these resources.

At CMU, we conducted a red teaming exercise by simulating real-world attack scenarios to identify, analyze, and exploit potential weaknesses across the hardware, software, network and cloud stack.

Our findings will inform targeted remediations to harden the device’s security, protect user privacy and reinforce trust in next-generation smart grid technologies.

Post Road Foundation: MTEP Chat and Voice Assistant

Homeowners with smart energy devices struggle to monitor and control their distributed energy resources (DERs) through multiple apps and interfaces, while also lacking understanding of technical energy management concepts. Our team developed a conversational voice assistant that enables users to naturally inquire about their solar panels, batteries, and HVAC systems through simple voice commands. It also provides educational support by explaining professional terminology and guiding users through system operations.

The system leverages advanced speech recognition and AI language models to understand user intent, query device databases and deliver both operational status updates and educational explanations in clear, accessible language within 10 seconds. This voice interface democratizes smart home energy management for users of all technical backgrounds, accelerating the adoption of sustainable energy technologies through improved understanding and ease of use.