I'd read about gappa in here : https://hal.inria.fr/hal-01534533/document https://hal.inria.fr/hal-01534533/document and then https://hal.archives-ouvertes.fr/h

I'd read about gappa in here : https://hal.inria.fr/hal-01534533/document https://hal.inria.fr/hal-01534533/document and then https://hal.archives-ouvertes.fr/hal-01522770/document https://hal.archives-ouvertes.fr/hal-01522770/document . Seems they're building on the work done with gappa. My guess (bystander and user of the tech) is that it'll stay hard for 5-10 years (slow progress of research projects, lots of lead bullets, and far more cores on our dev machines...). If you're motivated and are ready for semi-automated proof you can probably use lemmas (pre-proven properties) in Spark but if you can't find your lemmas in the Spark toolset, then good luck with Coq or Isabelle. Some encouraging stuff is going on in the FP static analysis world though, with projects like herbie (based on sampling only IIRC), the Tocatta lab, and I've heard some good things about numalis (start-up). Edit: seems Gappa can be integrated through why3, and seems they did some work on collabaration with alt-ergo so it seems it should be usable through Spark. Something to check in the next release :-D.