Proving Kruskal’s Algorithm in SPARK: When Generative AI Meets Formal Verification

Formal verification in SPARK offers mathematically guaranteed software, but it is well known that writing the necessary contracts and lemmas can be time-consuming and requires significant expertise. During my recent internship at AdaCore, I was tasked with an exploratory project: evaluating how effectively Generative AI can assist developers in writing and proving SPARK 2014 code.

Benchmarking AI on SPARK: From Sorting to Gale-Shapley

By experimenting with various AI models across different algorithms, I noticed that the quality of the generated proofs depended heavily on both the model and the algorithm's inherent complexity. For all my tests, I used Claude Code with models ranging from Sonnet 4.6 to Opus 5. This blog post is an opportunity to share some empirical observations regarding their ability to generate formal proofs.

Sometimes, the AI failed completely. For example, I attempted to complete the proof of the Gale-Shapley algorithm. To explain it simply, Gale-Shapley is a stable matching algorithm. An illustration is the matching of students to universities so that no student and no university would both secretly prefer each other to their current matches. When trying to prove Gale-Shapley using Sonnet 4.6, the model got stuck in an endless loop trying to satisfy the prover and ultimately hit its token limit. However, this was not a theoretical limitation; rather, Sonnet is a lighter, less capable model tier. When I switched to Opus 4.8 on the same problem, the results were quite impressive. In less than 30 minutes of coding time, the implementation was complete, and all postconditions were successfully proven. Ultimately, this demonstrates why it is crucial to carefully choose your model's capabilities depending on the complexity of the task you are trying to achieve.

Overall, I found that earlier iterations like Sonnet 4.6 were perfectly capable of proving "easy" algorithms like Merge Sort or Quick Sort, and implementing standard data structures such as linked lists. But the capabilities of these models are improving rapidly every month: Sonnet 5, for instance, was able to prove Gale-Shapley entirely from scratch.

I also observed that AI is better at building and proving a project from scratch rather than completing a preexisting one. The latter approach often creates friction, leading to a clunky integration and poor cohesion between the old and new code. This can be a problem as the development of high-integrity code rarely involves building code from scratch; the bulk of the work is maintaining and enhancing code. So, how do we use AI on legacy projects? One way could be to modularize just as you would with SPARK. You can isolate the feature you want to prove and give the AI a small, well-defined scope, rather than asking it to navigate through thousands of lines of historical context. This was not explored in this internship, though.

Tackling Kruskal’s Algorithm

To properly push the boundaries of what current AI models can achieve, I needed a non-trivial algorithmic challenge. I chose Kruskal’s algorithm for finding a Minimum Spanning Tree (MST). In graph theory terms, given a connected, undirected graph with weighted edges, Kruskal's algorithm finds a subset of the edges that connects all the vertices without any cycles (a spanning tree) while minimizing the total edge weight.

The algorithm operates greedily: it sorts all edges by weight and continuously adds the lowest-weight edge to the growing tree, provided it does not form a cycle with the already chosen edges. To illustrate this practically, imagine a network of cities (vertices) that need to be connected by fiber-optic cables (edges). Kruskal's algorithm finds the absolutely cheapest way to lay these cables so that every city is part of the exact same network, ensuring no redundant, cycle-forming cables are built.

I made this choice for several reasons. First, it needs to use multiple data structures, such as graphs and linked lists. This would be a great test to see if an AI can adhere to those structures and to SPARK's ownership model. In addition, the proof of the algorithm's correctness is non-trivial; in particular, standard mathematical arguments do not translate well to SPARK, meaning the AI would have to formalize it directly in SPARK.

Proving Kruskal requires establishing four properties on the generated graph: Inclusion (it is a subgraph), Connectivity (it is spanning), Acyclicity (it is a forest), and Minimality (it has the minimum possible total weight). The sheer number of properties to formalize, the various data structures involved, and the non-trivial nature of the correctness proof made it an ideal candidate for testing AI generation.

The initial phase consisted of modeling the problem. We defined a Graph structure as an adjacency matrix with bounded weights, alongside standard operations. I used the AI to produce the initial implementation and the basic contracts. The model excelled at this phase, rapidly generating the necessary Ada structures.

More importantly, the AI correctly applied SPARK-specific paradigms. It successfully used Ghost code and lemmas to assist the SMT solver, built mathematical connectivity models to propagate properties more easily, understood how to write valid loop invariants, and respected SPARK’s strict pointer ownership policies.

The Minimality Roadblock

While the first three properties (Inclusion, Connectivity, Acyclicity) rely on a very solid model of connectivity, the AI faced no fundamental difficulties with them. Producing this model can be difficult in practice and requires careful thought before implementation; however, once established, the path to proving these three properties is straightforward. Proving Minimality, on the other hand, is not a straightforward task. The Minimality property states that the weight of the tree produced by Kruskal is less than or equal to the weight of any other spanning subgraph.

Because Kruskal uses a greedy approach—always picking the lightest available edge that doesn't form a cycle—proving global minimality locally inside a loop is not trivial. Quite frankly, I was not expecting the AI to succeed here, as I did not see a clear path to automate this myself.

To solve this, the AI came up with a very clever mathematical trick: decomposing the total weight of the graph into sub-sums subject to weight restrictions. Let F_≤s be the graph F restricted only to edges of weight ≤ s. The total weight of a forest can be rewritten as the sum of the differences in its number of connected components:

Weight(F) = ∑ (from s=0 to Max_Weight-1) [ nb_comp(F_≤s) - nb_comp(F) ]

Because Kruskal always greedily picks the lightest available edge, its tree groups vertices together at least as fast as any other valid tree at any given weight limit. The AI was able to use this to prove constructively, without proof by contradiction, the minimality of the graph produced.

My personal experience and the caveats

Overall, I found that AI was very good at proving code in SPARK, but one has to keep in mind that I was focused on proving the correctness of algorithms whose both implementations and proof are widely documented on the internet, and so is the optimal playground for AI. Still, the AI took an unusual route here: this constructive proof of Kruskal minimality with the threshold formula seems to be inspired by the formalization of Kruskal's Algorithm for Minimum Spanning Forest (Haslbeck, Lammich, Biendarra, 2019) and is an impressive translation of its ideas into SPARK. This shows AI's great generalization properties. In the context of this internship, I have not attempted to use it to verify large industrial-grade codebases, and therefore cannot comment on its scalability.

Conclusion

Ultimately, successfully proving Kruskal’s algorithm demonstrates that Generative AI has crossed a significant threshold in formal verification, it is lowering the barrier of entry of using formal methods in software development projects. The fact that a model like Opus 4.8 can comply with SPARK's strict ownership rules, use Ghost code, and independently devise a clever mathematical workaround to prove global minimality is genuinely impressive. Models genuinely have a good understanding of what is and what is not provable in SPARK.