Rosette The Rosette Language

Applications

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.

Jitterbug A framework for writing and verifying just-in-time compilers.
SEEC A framework for reasoning about emergent computations.
SCFTL A framework for verifying a snapshot-consistent flash translation layer.
Serval A framework for developing automated verifiers for systems software.
Notary A verified device for secure transaction approval.
SwizzleInventor A framework for synthesizing swizzle GPU kernels.
MemSynth A language and tool for verifying, synthesizing, and disambiguating memory consistency models.
Ocelot An engine for solving, verifying, and synthesizing specifications in bounded relational logic.
Cosette A framework for reasoning about SQL equivalences.
Bagpipe A language for specifying BGP policies and verifying that an Internet Service Provider’s router configurations implement these policies.
Neutrons A verifier for a subset of EPICS. Currently in use at the University of Washington Clinical Neutron Therapy System.
Greenthumb A framework for constructing superoptimizers.
Chlorophyll A synthesis-aided programming model and compiler for GreenArrays GA144, a minimalist low-power spatial architecture.
Nonograms A system for synthesizing problem-solving strategies for logic puzzles.
Quivela A tool for proving the security of cryptographic protocols.
Ferrite A framework for specifying and checking file system crash-consistency models.
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.