Java PathFinder (JPF) is an Open-Source system contributed by NASA to verify executable Java bytecode programs. JDJ has an interesting article on it, "NASA Open-Sources Java Pathfinder." This is a somewhat historic moment, as this is the first Open-Source NASA program to be actively developed and hosted on SourceForge.