I've been reading about Ito Calculus, but most of it has been non-formal, applied stuff. They talk a bit about deriving Ito's lemma using Taylor expansion, and about Ito Integration. But they don't actually formally develop the Ito integral from the ground up. This is the best text I've found, but at the top of page 3, it still just "tells" you (without proof) what the squared variation of the Brownian motion is.
So my question is: do you have a good, clear text, that formally develops Ito calculus from the ground up, with proofs?
I very much like Lawrence C. Evans: An introduction to stochastic differential equations (AMS, ISBN 978-1-4704-1054-4). I admit, though, that I have mostly been reading the part of the book that comes after the introduction of Brownian motion and the Itô integral.