# CAREER: Formal Specifications as a Foundation for Aligned and Automated Software Engineering

> **NSF 01003031DB NSF RESEARCH & RELATED ACTIVIT** · University of Massachusetts Amherst (MA) · $689,531

## Abstract

Modern software increasingly relies on autonomous AI-driven systems that generate, test, and revise code. Yet even the most advanced tools struggle with a simple question: does the software behave as intended? The answer depends on clear descriptions of expected behavior, known as formal specifications. In practice, such specifications are rare because they are difficult to write and maintain. This project studies how to make formal specifications practical, accessible, and central to software development. The project’s novelties are the creation of a large-scale resource that connects everyday language descriptions, precise behavioral rules, and real code; automated methods that derive and update these rules as software evolves; and tools that use them to guide intelligent AI-based coding systems. The project’s broader significance and importance are that reliable specifications enable safer AI-based autonomous systems, reduce costly failures, and increase public trust in critical software infrastructure, including applications in healthcare and finance.

The project establishes a repository-level dataset linking natural language documentation, formal behavioral specifications, and code artifacts, accompanied by an automated evaluation pipeline for reproducible assessment of specification accuracy. It develops methods to infer specifications from documentation and program structure, propagate them across code dependencies, and maintain them under version changes to preserve semantic alignment. The project also advances specification-driven development tools that use these formal artifacts as semantic constraints to guide AI-based code generation and to detect behavioral inconsistencies early in the lifecycle. By integrating data infrastructure, inference algorithms, and alignment-oriented tooling, the research strengthens the theoretical and practical foundations of specification-centered software engineering. Its impact extends beyond computer science by enablin

## Key facts

- **NSF award ID:** 2542053
- **Awardee organization:** University of Massachusetts Amherst (MA)
- **SAM.gov UEI:** VGJHK59NMPK9
- **PI:** Juan Zhai
- **Primary program:** 01003031DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), CAREER-Faculty Erly Career Dev, SOFTWARE ENG & FORMAL METHODS
- **Estimated total:** $689,531
- **Funds obligated:** $396,112
- **Transaction type:** Continuing Grant
- **Period:** 07/01/2026 → 06/30/2031

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2542053

## Citation

> US National Science Foundation, Award 2542053, CAREER: Formal Specifications as a Foundation for Aligned and Automated Software Engineering. Retrieved via AI Analytics 2026-07-09 from https://api.ai-analytics.org/grant/nsf/2542053. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*