ImProve [1] is a imperative programming language for high assurance applications. Using Yices [2], ImProve verifies programs will always adhere to assertion specifications, irrespective of program input. If it is possible for an assertion not to be upheld, ImProve will emit a counter example in the form of a program trace, which illustrates how the assertion could be violated. This release improves the means to annotate programs for debugging (see 'label'). Also, the model checker now includes a pass to remove irrelevant statements, thus speeding up verification and making counter example traces easier to read. At Eaton, we have started using ImProve on critical chunks of code in our hybrid vehicles. To date we have ImProve generated C successfully running in a new prototype vehicle. In addition to finding a handful of minor bugs, ImProve has revealed two specification ambiguities arising from multiple, conflicting requirements. Due to the nature of the conflict, it is highly unlikely that the defects would have been identified with conventional testing. -Tom [1] http://hackage.haskell.org/package/improve [2] http://yices.csl.sri.com/