Krakatoa and Jessie are two front-ends of the Why platform for deductive program verification. Krakatoa deals with Java programs annotated in a variant of the The Java Modeling Language. Jessie deals with C programs annotated in the ANSI/ISO C Specification Language (ACSL). Technically, Jessie denotes two things: an intermediate language common to C and Java, and a plugin of the Frama-C environment which compiles ACSL-annotated C code into the Jessie intermediate language. The relationship between these tools are illustrated by the picture on the right.