there's also ats [http://www.ats-lang.org/]. somewhere on my long-term todo list is to write a library of efficient data strucures in ats, to take advantage of some of its safety guarantees.
I've had much better luck with exhaustive testing with Klee and related libraries (e.g. for testing multi-threaded programs).
For whatever reason, they map better to how I think about problems, and I've found it easier to develop new code that is testable within those constraints.
You could write tests as needed and when a test fails write types that make that failure as close to compile time as possible.
Another approach is to just write C code, either embedded in ATS files or in C files that are linked into ATS. Then slowly convert C to ATS as you feel comfortable.