I think it's very good in terms of being very honest and up front about the limits of confidence provided by formal proofs (which is not just applicable to this project, but to all attempts at formal verification).
Basically, whenever you are proving things, you have to be aware that you are entering the endless chain of turtles. This proof works, because proofs about modelchecking worked, which worked because proofs about abstract algebra worked, which again work, because proofs about sets work.
If any of these proofs is not proving what one wanted (either, because it is wrong, or because they prove something you did not want (potentially in very, very subtle ways)), your entire proof collapses. This is pretty much the danger of proving things.
A very interesting application can be found in the game 'singularity'. In this game, you are an artificial intelligence, and after enough studies of math and psychology, you can create a proof that no AI can ever exist. However, this proof contains a very, very, very subtle bug, which will stay hidden forever, probably.
So, stay aware that your proofs stand on a boatload of assumptions and other proofs and they might (in a rare, esoteric case) collapse and everything will be fine :)
I think that's making it sound a little more fragile than it actually is.
Within a system like Isabelle, the formalisation of each piece of the proof must remain relatively consistent with both the built-in proofs about fundamental mathematical structures, as well as the proofs that you have written.
I say "relatively consistent" because I don't have enough experience with the internals of Isabelle to say with certainty as to exactly how consistency is enforced. I know that types are enforced in a globally consistent way, for example.
That said, I have a high degree of confidence in the correctness of machine-checked proofs.
So I understand that your point is that you're taking some leaps of faith, and I agree to a point, but I think they are much more reasoned and considered leaps than you suggest.
