This is a project with the goal of designing and implementing a program modelling language that allows for the efficient evaluation of arbitrary static assertions about the program's behavior.
Right now, the project is still in the problem-solving stages, so it would be best to check out the wiki, where the current language design is being presented.