Statically verified >99% of benchmark contracts, including dependent, recursive and higher order ones. Integration with Racket underway.