Formal Proof that area of a rectangle is $ab$

This is a good question! On the face of it, it seems that before you can start being rigorous, you have to define precisely what you mean by the area of a rectangle. But this is just what you are trying to prove!

However, there is another approach: you define exactly the properties that you require of a reasonable area metric. Then you adopt these properties as your axioms, and use them to show that an $a \times\ b$ rectangle has area $ab$.

In a Euclidean plane, we would expect the following axioms to hold for a reasonable area metric on $a \times b$ rectangles (with $a, b \ge 0$):

$A1$: The area of a $1 \times 1$ rectangle is $1$.

$A2$: Any two congruent rectangles have the same area.

$A3$: If a rectangle $R$ is the union of disjoint rectangles $S$ and $T$, then the area of $R$ is equal to the sum of the areas of $S$ and $T$.

Given these axioms, I think we can show by induction that for rational numbers $a$ and $b$, the area of an $a \times b$ rectangle is indeed $ab$. But what about rectangles with irrational sides? I think this might require another axiom:

$A4$: If a rectangle $R$ contains a rectangle $S$, then the area of $R$ is not less than the area of $S$.

Otherwise you might be able to construct pathological area metrics using the Axiom of Choice. But I am open to correction on this.

If anybody can suggest corrections or improvements to this axiom set, feel free to post them as a separate answer, so they don't get lost in the comments.

In order to interpret lengths and areas as numbers, you have to fix a unit length and a unit area. The former is usually done by defining a coordinate system, whereas the latter usually defines the square of the unit length as the unit of area. But that square is a product, so the definition already assumes that the area of the $1\times 1$ square is $1$, which seems to be something you want to prove.

If you accept this kind of setup, then you can consider transformations of your rectangle which turn it into another rectangle of the same area but with the unit length as the length of one edge. In that case you can prove that the other edge will be the product of the original edge lengths. You can use a von-Staudt construction to express this product geometrically, based on the unit length.

One can also start from the following axioms:

$A1$: The area of a $a \times a$ square is $a^2$.

$A2$: Any two congruent shapes have the same area.

$A3$: If a shape $R$ is disjoint union of shapes $S$ and $T$, then the area of $R$ is equal to the sum of the areas of $S$ and $T$.

With these axioms at hand one readily finds the area of a rectangle with sides $a$ and $b$:

On the sides of the rectangle $ABCD$ build the squares $ABC_1D_1$ and $A_1BCD_2$. Let $D_3= (A_1D_2)\cap (C_1D_1)$.

Obviously the rectangles $ABCD$ and $A_1BC_1D_3$ are congruent. Therefore from our axioms one obtains: $$\begin{align} 2[ABCD]&=[DD_1D_3D_2]-[ABC_1D_1]-[A_1BCD_2]\\ &=(a+b)^2-a^2-b^2=2ab. \end{align} $$