Behaviors as the backbone of software correctness

Gabriela Moreira introduces Quint, a language built on top of TLA+ to make formal specifications more accessible. Quint was designed at the blockchain company Informal Systems to solve the syntax and usability problems of TLA+.

Her talk focuses on the process of defining correct behavior in software, and then keeping that definition in view throughout the development process, demonstrating how specifications can stay alive throughout development through conformance testing, model-based testing, and trace validation. She introduces techniques for building confidence in specifications including modeling failures explicitly, using witnesses for vacuity checks, and creating reproducible examples that serve as trusted documentation. She also demonstrates how AI can help generate test harnesses and specifications using Quint, making formal methods more practical and accessible to development teams.