The Amiga Hand was the boot screen, not an error screen. You're thinking of the famous Guru Meditation.
Besides, who says that the Amiga kernel did _not_ meet the specifications? Have you read them? Does it mention "crash free" anywhere?
The Haskell code is called a "specfication", but if it is Haskell code, surely it should count as a _program_ already? How can you prove that that program is bug-free? How about conceptual bugs?
Was the toolchain verified? How about the hardware on which it runs?
What overhead does this approach have? Are the benefits worth it?
I'm not saying this is all bullshit, but it looks like me that they are pointing to one program, calling it a "specification", and then demonstrating machine translation / verification to a similar program. I'm not sure if I buy that methodology.