Skip to content

Software Quality

AI tooling for types and effects

Every method in this family has a checker that can refuse the answer, so AI proposes and the compiler or the solver decides. The field moves quickly, and these entries may be out of date.

Type systems

General coding assistants (Copilot, Cursor, Claude Code, Aider) are the de-facto workflow for type completion and JS→TS / Python→mypy migration. TypeT5 (Wei et al. 2023)1 infers Python types and beats the earlier HiTyper / Type4Py line. The checker's guarantee stops at shape: annotations that type-check are frequently wrong about intent (Yee and Guha 2023)2.

Linear types

rustc with an LLM in the loop is the de-facto workflow: the compiler is the oracle, so AI cannot ship a memory-unsafe program without writing unsafe. C→Rust translation at scale is active research — DARPA's TRACTOR program and LLM-repair extensions to the classical C2Rust pipeline.

Refinement and dependent types

The SMT solver is the oracle. Laurel (Mugnier et al. 2025)3 writes the helper assertions a failing proof needs, and Clover (Sun et al. 2023)4 checks a function against its docstring and its annotations; both target Dafny. AutoSpec (Wen et al. 2024)5 and SpecGen (Ma et al. 2024)6 target C/Java spec generation.

Effect systems

No AI tool proposes effect annotations: Koka, Eff and Unison are small enough that a model sees little of their code in training.

References

  1. Wei, Jiayi, Greg Durrett, and Isil Dillig. 2023. TypeT5: Seq2seq Type Inference using Static Analysis. https://doi.org/10.48550/arXiv.2303.09564. ↩

  2. Yee, Ming-Ho, and Arjun Guha. 2023. "Do Machine Learning Models Produce TypeScript Types That Type Check?" Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). https://doi.org/10.48550/arXiv.2302.12163. ↩

  3. Mugnier, Eric, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2025. "Laurel: Unblocking Automated Verification with Large Language Models." Proceedings of the ACM on Programming Languages, 1519–45. https://doi.org/10.1145/3720499. ↩

  4. Sun, Chuyue, Ying Sheng, Oded Padon, and Clark Barrett. 2023. Clover: Closed-Loop Verifiable Code Generation. https://doi.org/10.48550/arXiv.2310.17807. ↩

  5. Wen, Cheng, Jialun Cao, Jie Su, et al. 2024. "Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification." Formal Methods for Software Engineering (SEFM 2024), Lecture notes in computer science, 302–28. https://doi.org/10.1007/978-3-031-65630-9_16. ↩

  6. Ma, Lezhi, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2024. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. https://doi.org/10.48550/arXiv.2401.08807. ↩