This repository contains a version of the Java Class Library (rt.jar) that can be used together with JBMC to model-check Java code that calls the standard library.