I can't answer all of these questions authoritatively, as I have more of a systems focus than a formal methods focus, but I can hopefully point you in the right directions. The various published papers and final release will be the right places to find all the authoritative answers.
1) Why not use the Haskell version?
The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never against real hardware. Haskell has a complex runtime which is not (easily) suitable to run directly on Hardware (although one student I worked with did port a subset of the Haskell runtime to work on top of seL4). Using Haskell directly would be slow, and would require the researchers to prove the correctness of the Haskell runtime implementation as well which would be a huge amount of work.
2) What did you use to check the haskell version? I was not directly involved in this. I believe the Haskell used to write the kernel was a subset of the language, they call "literate haskell" which was used to both implement and specify the kernel. This was somehow minimally translated into a dialect of Isabelle called HOL.
3) What did you use to check that C implements what haskell implements?
A similar process was used for checking that the C implementation was a refinement of the Haskell. Again, a restrictive subset of the C language a tool was written to translate the C code into HOL (I think). I remember the team lead arguing that the way the C implementation was checked, both the code itself and the translator could be checked for bugs.
AFAIK, The tooling was almost all custom except for relying on Haskell and the Isabel theorem prover. The group had a lot of experience for building and releasing the OKL4 kernel so a lot of the dirty work was already done as well as an excellent "Advanced Operating Systems Course" which whips and tortures undergraduates into systems engineers and ideally PhD students. :-)
I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/, but due to limited scope (mostly functions of several hundered bits input and output as customary in crypto-primitives), they were able to check that the implementation adheres to specification automatically. The aim was to allways know that the c code does what it is supposed to, so that programmer can focus on mitigating side-channel attacks :)
I wonder if something similar would be applicable to writing the micro-kernell.
1) Why not use the Haskell version? The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never against real hardware. Haskell has a complex runtime which is not (easily) suitable to run directly on Hardware (although one student I worked with did port a subset of the Haskell runtime to work on top of seL4). Using Haskell directly would be slow, and would require the researchers to prove the correctness of the Haskell runtime implementation as well which would be a huge amount of work.
2) What did you use to check the haskell version? I was not directly involved in this. I believe the Haskell used to write the kernel was a subset of the language, they call "literate haskell" which was used to both implement and specify the kernel. This was somehow minimally translated into a dialect of Isabelle called HOL.
3) What did you use to check that C implements what haskell implements? A similar process was used for checking that the C implementation was a refinement of the Haskell. Again, a restrictive subset of the C language a tool was written to translate the C code into HOL (I think). I remember the team lead arguing that the way the C implementation was checked, both the code itself and the translator could be checked for bugs.
AFAIK, The tooling was almost all custom except for relying on Haskell and the Isabel theorem prover. The group had a lot of experience for building and releasing the OKL4 kernel so a lot of the dirty work was already done as well as an excellent "Advanced Operating Systems Course" which whips and tortures undergraduates into systems engineers and ideally PhD students. :-)