Rosette puts a solver inside Racket and splits the language in two

A Racket extension aimed at synthesis and verification

Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification and more. The repository holds the source of the language itself along with several example solver-aided DSLs, and the README is explicit that this is the language project rather than a tool that wraps an existing solver.

The audience is narrow and specific: programmers who already think in Racket and who want to write a property, a specification or a search over programs in the same language as the rest of their code. The project's own documentation points at two references for depth, a Rosette Guide hosted with the Racket documentation and a PLDI 2014 paper describing the internals, which tells you the design has been written up rather than merely shipped.

The interesting part is not that a solver exists, since plenty of solvers exist, but how the language is built around one. Rosette adds a notion of symbolic values to the host language, and the whole design question becomes what happens when a value that is not a concrete number meets a Racket operation that expects one. The two-language split in the next section is the direct answer to that question.

Two languages, and the safety burden moves to the programmer

Rosette ships two languages, #lang rosette/safe and #lang rosette, and the difference between them is the most consequential decision in the project.

The safe language includes only constructs that are safe to use with symbolic values. For now that excludes some convenient Racket features, such as iteration constructs. The README argues that the semantics of those constructs can be expressed in the core language, so nothing is lost except convenience, and it recommends that new users start with rosette/safe. You can ask the REPL what is on offer.

> (rosette)
'(define assert let let* ...)

The full rosette language includes all of Racket, and the README is blunt about the consequence: the burden falls on the programmer to decide whether a given construct is safe in a given context, because Rosette provides no guarantees or checks for programs that use unsafe constructs. The failure modes are described in order of severity. In the best case the program throws an exception when a symbolic value reaches a construct that does not support it. In the worst case it keeps running with incorrect semantics, or does something more serious such as writing incorrect data to a file.

That second failure mode is the one to remember. This is a language where a missing check can turn into silent wrong answers rather than a crash, and the safe language exists precisely to keep you out of that territory.

Installing through raco, with Racket 8.1 as the floor

Rosette installs as a Racket package, and the README calls that the easiest route. The requirement is Racket 8.1 or later, downloaded from racket-lang.org, after which the package manager handles the rest.

$ raco pkg install rosette

Installing from source follows the same shape. Clone the repository, remove any previous version of Rosette so the two do not collide in the package cache, and install from the checkout.

$ git clone https://github.com/emina/rosette.git
$ raco pkg remove rosette
$ cd rosette
$ raco pkg install

The ordering matters more than it looks. The removal step is listed separately from the install because Racket keeps installed packages in a shared location, and installing over an existing Rosette is the kind of thing that leaves a stale package behind. The from-source route is what you need when you intend to modify the language or work on the bundled DSLs, and the package manager route is the right choice for using them.

Nothing in the README describes a binary distribution or a standalone installer, which is consistent with how a Racket extension is meant to be shipped.

The container build fixes Racket 8.4 with the Chez variant

The repository includes a Dockerfile, and it shows how the project itself is packaged for repeatable environments. It starts from Alpine 3.15 and pins the Racket version and variant as build arguments.

FROM alpine:3.15
ARG RACKET_VERSION=8.4
ARG RACKET_VARIANT=cs

The variant argument can be cs for Chez Scheme, bc for Before Chez, or natipkg where external libraries are included in the Racket packages. The default is cs. System packages gcompat and ncurses are added first, with a comment explaining that gcompat is needed for Racket and ncurses for the xrepl and expeditor packages that provide the REPL. The installer script is downloaded, run with a piped answer sequence, and removed again.

RUN apk add --no-cache gcompat ncurses
RUN raco setup --no-docs
RUN raco pkg install -i --batch --auto --no-docs expeditor-lib

After that the image copies the two info.rkt files, one at the root and one for the rosette subdirectory. The Dockerfile explains why: installing Rosette from only those files would fail, but they are enough to resolve the dependency set. The image then works in /usr/local/rosette, a directory the comment notes is cleaned up later so its location is not important.

This is a well-constructed build for a research language, and it is also a hint about the real deployment shape. Rosette lives inside the Racket package system, and the expeditor REPL package is a deliberate part of that setup rather than an afterthought.

DrRacket first, raco make and racket from the shell

The README gives execution instructions that reveal the intended workflow. The primary route is to open a program in DrRacket and run it, with the bundled finite state machine demo at rosette/sdsl/fsm/demo.rkt given as the example target. DrRacket is described as the preferred way to execute Rosette programs.

For the command line, the instruction is to compile the program first, then run it.

$ raco make <your program>
$ racket <your program>

The compile step is not optional in that description. Running a .rkt file directly with racket will compile it on the fly, but the README asks you to run raco make first, which in a Racket project means producing the compiled artefact and reporting compile-time errors before execution starts. For a language where the compiler and the solver interact, that ordering is the difference between a syntax error and a type error.

The repository layout supports the same story. The rosette/ directory holds the language implementation and its own info.rkt, sdsl/ holds the example solver-aided DSLs, test/ holds tests, and there is a .github directory with a Tests workflow badge at the top of the README. The .github workflow suggests continuous integration is wired up, and the presence of a top-level info.rkt is what makes the whole tree installable as a Racket package.

Sample DSLs are the intended path into the language

A solver-aided language is hard to evaluate with hello-world examples, and the project knows it. The bundled solver-aided DSLs exist to give you something substantial to read, and the finite state machine demo under rosette/sdsl/fsm/ is the one the README points at first.

The value of these examples is that they show the intended shape of the work: you describe a system in a domain language, express a property, and let the solver reason about the symbolic state of that system. The DSLs in this repository are samples, and the README says as much, so they are best treated as worked examples to learn the style from rather than as production libraries to depend on.

There is also a NOTES.md file at the top level, which usually means developer-facing commentary that is not polished documentation, and a LICENSE file that GitHub cannot classify. That last point is worth pausing on. The project is not under a standard OSI licence, so a team considering it needs to read the LICENSE file and decide for itself what the terms allow. Nothing in the repository suggests a permissive or a copyleft grant, and the README does not describe the terms in prose.

Releases stopped at 4.1 while commits kept arriving

The published releases are old. Version 3.2 came out on 2021-03-04, version 4.0 on 2021-03-12, and version 4.1 on 2022-03-08. Nothing newer has been tagged since.

The repository, however, has not been idle. The last push to the master branch was on 2026-10-16, which is well past the last release tag. That combination is typical of an academic language project that keeps receiving fixes and improvements on the default branch without cutting new release tags, and it has a direct consequence for users: the version you get from the Racket package manager and the version in the git checkout can differ, and the checkout is the newer one.

So the upgrade cost of this project is not a package upgrade but a source upgrade. If you are on 4.1 from the package manager and the checkout has moved on, you are choosing between a tagged snapshot and unreleased changes, and nothing in the repository, no changelog and no tag, tells you what the difference is. That is the main thing to verify before depending on Rosette for anything long-lived: compare the tagged release against master and see whether the changes matter to your use.

Editorial conclusion

Rosette suits a Racket user who wants to state a property and let a solver search for a counterexample or a program, and it does not suit a team that needs its verification tooling in a language other than Racket or a solver integration it controls itself. Before adopting it, read the LICENSE file yourself, since the project ships a custom licence that GitHub cannot classify, and start with #lang rosette/safe rather than the full language, because the safe subset is the one that fails loudly when a symbolic value reaches an unsupported construct.

Frequently asked questions

Official sources

1. emina/rosette on GitHub
2. Issues
3. README
4. Releases