Finished writing up solutions to the hardest logic puzzle ever:

A simple solution to the hardest logic puzzle ever (with Brian)

Still working on a formal system to make the proofs symbolic (i.e trivial). Just need restricted indexicals (ranging over True/False/Random) and a couple new truth values (Explode and Indifferent) to deal with the self-reference.