The Rosette Language


Rosette hosts many domain-specific languages (DSLs) with advanced programming tools that scale to real-world applications, from verification of radiotherapy software to synthesis of code for ultra-low power hardware. Several of these tools have been developed by first-time users of Rosette in just a few days or weeks.

Bagpipe A language for specifying BGP policies and verifying that an Internet Service Provider’s router configurations implement these policies.
Chlorophyll A synthesis-aided programming model and compiler for GreenArrays GA144, a minimalist low-power spatial architecture.
Cosette A framework for reasoning about SQL equivalences.
Ferrite A framework for specifying and checking file system crash-consistency models.
Greenthumb A framework for constructing superoptimizers.
Neutrons A verifier for a subset of EPICS. Currently in use at the University of Washington Clinical Neutron Therapy System.
Synapse A framework for specifying and solving optimal synthesis problems.
Wallingford An experimental constraint reactive programming language.
More Demo languages and tools for secure stack machines, data-parallel programing, and web-scraping.