JavaFE is a Java front-end that parses Java 1.4 source code and Java 1.5 bytecode. It is used as a compiler front-end for several research tools, including ESC/Java2 and RCC. JavaFE has a partial formal specification and, because it is a hand-written lexer, parser, and type checker, is very efficient.
Votail is an implementation of Ireland's method of Proportional Representation by Single Transferable Vote (PRSTV). The functional requirements derived from Irish electoral law are specified using Business Object Notation (BON) and the Java Modeling Language (JML). Formal methods have been used to verify the correctness of the software.
See the Votail paper at FoVeOOS 2010