Praxis and AdaCore have announced the formation of a long-term partnership with the intent of enhancing the capabilities of the Spark language and toolset. This announcement follows the recent release to the open-source community of the Tokeneer project by the US National Security Agency (NSA). This project was developed by Praxis for the NSA using Correctness-by-Construction methodology, the Spark Ada language and toolset and the GNAT Pro Ada development environment from AdaCore. Praxis' Correctness-by-Construction methodology helps yield higher productivity, lower defect rates and lower support costs for high assurance software. The methodology is based on a number of principles, such as the expectation that requirements will change, elimination of errors before testing, incremental development, and writing software that is easy to verify.