IBM also has a GraphBLAS [1] implementation in the works [2], and this summer Jenna Wise [3], a PhD candidate at CMU, spent the summer at IBM working on a formal verification proof of the GraphBLAS code [4].

[1] http://graphblas.org

[2] IBM GraphBLAS https://github.com/IBM/ibmgraphblas

[3] Jenna Wise, CMU http://www.cs.cmu.edu/~jlwise/

[4] Formal verification proof of the GraphBLAS C API https://github.com/jennalwise/graphblas-verif