JmlOk2 JmlOk2 is a tool for detecting and classifying nonconformances in contract-based programs, tailored by Java/JML. More details can be found in tool's website: http://massoni.computacao.ufcg.edu.br/home/jmlok