Loyola University Chicago
B.S. in Computer Science, minor in Information Systems
Completed May 2026
Dean's List, Mulcahy Scholar for LLM-based TLA+ research, and Presidential Scholarship.
Curriculum Vitae
Eric Spencer's education, software engineering experience, and research publications in formal methods and large language models.
I work on formal methods and large language models with Loyola University Chicago's AI4FM group, alongside software engineering at HorneSci and independent software through FROM AMERICA LLC.
Education
Experience
Member of Technical Staff · HorneSci
Jun 2026 – present
Technical discovery and delivery for customer integrations of the Hierarchical Sparse Transform, working across C++, Java, Python, and Kafka event pipelines.
Founder · From America
May 2026 – present
Product direction, licensing, and development for independent software ventures.
Researcher · AI4FM · Loyola University Chicago
Aug 2025 – present
Research on generating and evaluating TLA+ specifications with language models. The work connects generated specifications to SANY parsing and TLC model checking, and includes the released chattla-20b model.
Software Engineer · CCC Intelligent Solutions
May 2025 – Aug 2025
Software engineering internship building a claims portal and operational dashboard with Vue.js and Spring Boot.
Manager, Marketing CX Study · Microsoft
Jan 2025 – Dec 2025
Software Engineer · EpiFinder, Inc.
Jan 2025 – May 2025
Software engineering internship automating HR data, permissions, and email-based access requests with Google Apps Script.
IT Services Desk Technician · Loyola University Chicago
Jul 2024 – May 2026
Technical support for students, faculty, and staff, including access provisioning and incident investigation with infrastructure teams.
Undergraduate Research Assistant · Loyola University Chicago
May 2023 – Aug 2023
Studied language-model comprehension of advanced Java concepts and contributed to experimental design and documentation.
Publications
- TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
2026 · arXiv preprint, arXiv:2607.23425 - TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
2026 · ICSOFT 2026, pp. 627–636 - Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
2026 · ICSOFT 2026, pp. 39–50
Full CV
The PDF includes the full list of roles, projects, and technical skills.