Just to make sure that people don't get the wrong idea;

Nada Amin's Harvard webpage states;

I combine programming languages (PL) and artificial intelligence (AI), including large language models (LLMs), to create intelligent systems that are correct by construction. My current application domains include program and proof synthesis, and precision medicine. ... we look at combining Machine Learning and Programming Languages to enable the creation of neuro-symbolic systems that can move back and forth between learnable (neural) and interpretable (symbolic) representations of a system.

She was a recipient of the Amazon Research Award 2024 for LLM-Augmented Semi-Automated Proofs for Interactive Verification - https://www.amazon.science/research-awards/program-updates/7...