Any performance benchmarks you could share? I think the trade-off for program correctness is worthwhile, but I wished to see more theorems around the core business logic