Rosette, an internal DSL for verification and synthesis

Someone just pointed this out to me.
It is an extension of Racket used for verification and synthesis.

In this video at minute 42 they present some applications of the DSL which seem interesting.

I will need to dive more into this, but this could be of interest to @voelter and @sergej , given the discussion on Racket