What is SPARK?

• Deductive program verification for the SPARK language - an Ada-derived language with broad coverage of Ada features
• Practical, modular, scalable verification for systems and embedded programs
• Professional, industrial-strength formal methods

What’s it like to use SPARK?

• Building a safety monitor for a M.A.R.S Rover
• Automatic proof for the autonomous mode
• Discovery of an error in the remote-control mode

The Future: SPARK and Generative AI

• SPARK: the best possible language to use for Generative AI