Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

I didn’t see this mentioned anywhere yet. Would appreciate comments/review by “SPARK knowledgeable” people.

3 Likes

A quick review finds some sloppiness, in that they misspell Yannick Moy’s last name (as “Moi”) and their reference for the Ada Programming Language is to:
“AdaCore (1980). Ada programming language. ada-lang.io, an Ada community site | ada-lang.io, an Ada community site
which is triply amusing since (1) AdaCore didn’t exist in 1980, (2) the Ada we know of today originates from 1983 or 1987, and (3) ada-lang.io (despite having a nice rendition of the Ada RM) is not in any sense the official place to find the International Ada Standard.

2 Likes