Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity. Stating that some valu

Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity. Stating that some value is the gcd is surprisingly tricky. Once you have proven that Bézout's identity holds for your function you could prove it is the actual gcd by showing it is a divisor for both a an b. Assuming I understood the notation correctly that would give something like the following lemma euclid_gcd(nat: a, nat: b) ensures (a % GCD(a,b)) == 0 ensures (b % GCD(a,b)) == 0 { } I'd be curious to know if it can prove this. Note that this would still not constitute a proof of Bézout's identity, as it uses it to define what the gcd is. Thankfully defining the gcd using Bézout's identity is pretty common nowadays, as it allows for a useful generalisation of the concept.