Using Spark to Prove 255-Bit Integer Arithmetic from Curve25519

One of the most important functions used in the proof is a function that converts the array of 10 integers to the big integer it represents, so when X is an Integer_255 then +X is its corresponding big integer. Another case of inductive reasoning in my project is a lemma, whose proof present a very useful technique when proving algorithms using recursive ghost functions in contracts. I had a lot of recursive functions in my contracts, but also quantifiers… I did not hesitate to split proofs into Ghost procedures in order to reduce context size, but also wrap some expressions into functions.

Source: blog.adacore.com