JayHorn is a software model checking tool for Java. JayHorn tries to find a proof that certain bad states in a Java program are never reachable. These bad states are specified by adding runtime assertions (where some assertions may be generated, e.g., that an object reference must not be Null before being accessed). JayHorn tries to err on the side of precision that is, when it is not able to proof that an assertion always holds, it will claim that the assertion may be violated (this is called soundness). JayHorn is currently sound (modulo bugs) for Java that use a single thread, have no dynamic class loading, and do not perform complex operations in static initializers.