JA Form SSJ_AdaCore_Redacted.pdf

This is a Single Source Justification (SSJ) document for a sole source procurement below the Simplified Acquisition Threshold (SAT) by the Air Force Research Laboratory (AFRL).

The Government requires a sole source purchase of software licenses and support from AdaCore Technology for a one-year license period from May 31, 2026 through May 30, 2027. The required products are GNAT Pro, GNAT DAS (Dynamic Analysis Suite), and SPARK Pro—code verification software specific to AdaCore. The contracting activity is AFRL/PZLET under the AdaCore-GNAT Pro/SPARK Pro/GNAT DAS project, utilizing FY26 3600 Funds. The estimated contract cost is redacted in the document.

The justification establishes that SPARK Pro is the only product capable of feasibly verifying the Government's Ada/SPARK software used in unmanned aerial vehicle systems. AFRL/RQA conducted a pilot program evaluating formal software verification solutions; SPARK Pro was the sole product meeting verification requirements. The rationale emphasizes that competing products cannot verify necessary software properties with reasonable effort, and that substantial duplication of effort (redacted years) would be required to develop equivalent capabilities in alternative programming languages. The Contracting Officer's determination, dated April 10, 2026, cites FAR 13.106-1(b)(1) as the regulatory basis for the single source award. The document indicates continued market research will monitor whether alternative sources become available to preclude future single source awards.