Smoosh - The Symbolic, Mechanized, Observable, Operational Shell

By Michael Greenberg with Austin Blatt and Calvin Aylward

Smoosh (the Symbolic, Mechanized, Observable, Operational SHell) is a formalization of the POSIX shell standard.

The formal model can run in a purely symbolic mode, working with a model of a POSIX system.
The formal model is code, written in Lem.
The formal model uses small-step operational semantics and produce a trace of how the shell evaluated a given term.
The formal model can run in a non-symbolic mode, making real system calls via OCaml drivers.
The formal model's drivers yield a functioning, POSIX compliant shell.

Demo: the web-based 'shtepper'

As a trial of Smoosh's capabilities, we've built a web-based shell stepper (a/k/a the 'shtepper') that can symbolically step shell code through the various phases of expansion and evaluation.

The implementation of commands is limited to the core builtin operations of the shell; the filesystem and unknown executables are treated symbolically.


Smoosh's source code is open (MIT licensed) and freely available. The repository has several Dockerfiles to help you get started.


The POSIX shell is an interactive DSL for concurrency
Michael Greenberg, DSLDI 2018. An argument for understanding the shell as a DSL for managing concurrent tasks; the first demo of the Smoosh shtepper.
Word expansion supports POSIX shell interactivity
Michael Greenberg, PX/2018. An argument about how the shell's use of word expansion dovetails with the shell's interactivity.
Understanding the POSIX Shell as a Programming Language
Michael Greenberg, OBT 2017. The initial proposal of the Smoosh project.

Cite Smoosh

No paper has yet been published on Smoosh's semantics. To cite Smoosh as an artifact, please use:

  title = {Smoosh: the Symbolic, Mechanized, Observable, Operational Shell},
  author = { Michael Greenberg },
  year = 2019,
  url = {},
  note = {Current version: 0.1}