The work on the K project was or is partly supported by the following academic grants and contracts (reverse chronological order, by start date):
- NSF CCF-1318191. SHF: Small: VeriF-OPT, a Verification Framework for Optimizations and Program Transformations. $466,000 for 2013-2016.
- Rockwell Collins. Semantics-Based Analysis Framework for C. $125,000 for the period 2012-2013.
- DARPA HACMS. Design and Assurance for the Modular Assembly of Sense Control – Actuate Systems (DAMASCAS). Joint project with SRI International (CSL). UIUC share $1,657,807 for 2012-2017.
- Boeing. Formal Analysis of Real-Time Distributed Systems. $240,000 for the period 2012-2013.
- NSF CCF-1218605. SHF: Small: Usable Verification using Rewriting and Matching Logic. $400,000 for 2012-2015.
- Google Summer of Code (FSL was an accepted organization). K Framework. $24,000 for Summer 2012.
- NSA. Formal Verification of C Programs using Rewriting Logic Semantics and Matching Logic. $754,000 for 2010-2013.
- DAK. An Executable Semantic Framework for Rigorous Design, Analysis and Testing of Systems. EU funded, Romanian Contract 161/15.06.2010, SMISCSNR 602-12516.
- Microsoft Research gift. $35,000 (Recommended by James Larus) in 2007.
- Microsoft Research gift. $15,000 (Recommended by Tom Ball) in 2007.
- Microsoft Research gift. $10,000 (Recommended by Wolfram Schulte) in 2005.
Additionally, Runtime Verification, Inc., with funding from NASA and Toyota, is a regular contributor to the design and the development of K.