From Formal Requirements to Compositional Assurance: Functional Models, Machine-Checked Proofs, and Digital Twins
November 18, 2026 · 10:00 a.m.
University of Alabama in Huntsville · OKT N132
Abstract
As engineering systems become increasingly complex and artificial intelligence accelerates software development, how can we establish confidence that individually correct components will behave correctly when combined?
This talk explores the intersection of functional modeling, formal requirements, and machine-checked reasoning using Lean, a modern programming language and theorem prover. Through accessible examples from software engineering and digital twins, it examines how mathematical specifications and compositional reasoning can strengthen engineering assurance.
The discussion highlights opportunities for collaboration between computer science and industrial and systems engineering, particularly in developing systems whose correctness arguments can evolve alongside their designs.
About the Talk
Correct components do not necessarily compose into a correct system.
Using Lean, this seminar explores how formal specifications, component contracts, and machine-checked proofs can expose requirements that ordinary interfaces do not capture.
Examples include mergesort and a manufacturing digital-twin scenario inspired by published research on an automotive pallet elevator.
The talk also introduces Compositional Autoformalization as a prospective research direction combining AI-assisted formalization of engineering models with machine-checked assurance of their composition.
Presentation Materials
The presentation slides, selected Lean examples, and supplementary references will be made available here.
Selected References
- Wooley, A., Bitencourt, J., and Silva, D. (2025). Bridging the Gap Between Discrete Event Simulation and Digital Twin: A Manufacturing Case Study. Manufacturing Letters, 44, 1274–1284.
- Morris, J. H., Gibbons, D. W., Gregory, J., and Mocko, G. (2026). Technical Strategies for Semantic Aggregation of Interoperable Digital Twins. Conference on Systems Engineering Research.
Speaker
Greg Bacon, Ph.D. is CTO of OASYS, INC., an employee-owned defense technology company in Huntsville, Alabama, and an adjunct faculty member in the Department of Computer Science at UAH. His professional and academic interests include software engineering, systems engineering, formal methods, and artificial intelligence.