If you want to eliminate any hand-waving, then use a mechanized theorem prover. A significant book series in this area that's also available online is Benjamin Pierce's Software Foundations series. This series teaches you how to use the proof assistant Coq, the system used for (among many other things) formally verifying the CompCert C compiler, for computer science problems including algorithm verification. From there Coq libraries like YNot and the research/publications around them would be a place to look.
There are also mechanized theorem provers or related tools that take different approaches. Things like Frama-C, Why3, Alloy, Spin, Ada SPARK, the $\mathbb{K}$ Framework, NuPRL, Isabelle/HOL, Twelf, TLAPS, Welder/Inox and many others. These approach different aspects of the problem with different approaches and different levels of ambition and usability. For example, to prove something about a program, you need to have a semantics for the programming language. Simplifying the creation of programming language semantics is the goal of the $\mathbb{K}$ framework meanwhile Ada SPARK is a large fragment of Ada with a formal semantics. Specifying the semantics of C and assembly in Coq was a huge part of the CompCert project. Given a semantics, you then need some way of giving a specification of your program and generally connecting the source code. Frama-C does this for C (and there are variations in that suite for other languages). Of course, stating what you expect is different from proving that it holds. Proof assistants like Coq, Twelf, Isabelle/HOL, and TLAPS allow very complicated theorems to be proven but require a fairly high level of expertise to use in real world cases. These also take different approaches using either constructive type theory, classical higher-order logic, or set theory. In many cases, what needs to be proven is relatively simple and can be fully automated. Tools like Welder/Inox coordinate automatic theorem provers to deal with these. Sometimes its just too expensive/difficult to get (and crucially maintain) a full proof of correctness. Model checkers like Spin and Alloy can be used to exhaustively check the state space of the program (or an abstraction thereof) at least to some depth. These can often find defects, and in some cases may be able to fully check the state space. These are much easier to use but they don't give the same guarantees and can take huge amounts of computation. In practice, they are often used to verify protocols rather than the actual code to minimize the state space. A different approach to trying to prove code correct is to extract the program from a proof. NuPRL is one of the oldest, still living systems that focuses on this approach, but this can be done with Isabelle/HOL and Coq as well. Some systems like Why3, Welder, and Isabelle are more frameworks meant to help join tools together. There are many other alternatives to the tools that I've listed in each of their niches.
Best Answer
Hints:
In the Euclidean algorithm, the decay of the variables is obtained by the division of the largest by the smallest, using $a=bq+r$ i.e. $r=a-bq$, then swapping $a,b\to b,r$, as long as $q>0$. It is clear that the worst case occurs when the quotient $q$ is the smallest possible, which is $1$, on every iteration, so that the iterations are in fact
$$a,b\to b,a-b.$$
If you reverse this assignment, you get
$$a,b\to a+b,b$$
and you obtain the recurrence relation that defines the Fibonacci sequence.
Hence the longest decay is achieved when the initial numbers are two successive Fibonacci, let $F_n,F_{n-1}$, and the complexity is $O(n)$ as it takes $n$ step to reach $F_1=F_0=1$.
Now we know that $F_n=O(\phi^n)$ so that $$\log(F_n)=O(n).$$