Is there a formlisation of Euclidean geometry?

What I mean is this: Is there a formalisation into which we can embed
Euclid's Elements (or at least a non-trivial part of it) in such a way
that the proofs could be checked by machine? It could be done in an
uninteresting way simply by using R^2 as a model of the plane and
using the axioms of ZF. But is there a formal axiomatisation that is
close to what Euclid attempted? Obviously Euclid thought he had
achieved this goal, but it's not clear at all you can really reduce
his proofs to deductions from just his five axioms.
.