This is a workshop repo designed to help engineers learn about spec-driven development (and lightweight formal methods) through a series of exercises.
For more details, see the main guide and reference. See the main-more branch for... more.
The base tooling depends on:
- GNU Make 4.x or better (Make 3.x will also work on most platforms)
- GNU Bash 3.x or better
- Java 21 or better
- Maven 3.6 or better (this project should be compatible with Maven 4)
This project uses Make to manage build/project commands.
Attention! You must run these commands first before using the project. Please have a good internet connection before continuing.
make toolingmake check
- The project uses Maven for managing dependences and workflow plugins
- Code formatting with Spotless; Currently using the Palantir-modified Google Style
- Unit tests via JUnit5, property-based tests via jqwik, concurrency tests via Fray -- all integrated through JUnit5
- Static analysis via Google Errorprone, Spotbugs, and find-security-bugs
- Extended checking and verification with OpenJML
As you adapt the spec-driven techniques to other languages and runtimes, you should have similar tooling coverage. For example, in Rust you might use Cargo, rustfmt, proptest/quickcheck/bolero for property-based tests, Shuttle for concurrency tests, clippy and cargo-audit for additional static analysis, and Kani/Prusti/Creusot for verication. Kani integrates directly with Bolero (so that might make the tooling a bit easier) and presumably the test suite would be run with Miri.
make tooling- downloads all required tools for this projectmake clean- deletes all build/test artifactsmake format- runs the code formattermake check- runsformatand then compiles all code and tests, runs all static analyzers, runs the test suitemake check-jml- runscheckand then runs full JML code verificationmake doc- produces API / Javadoc documentationmake jshell- launches an interactive JShell (full Classpath access)make repl- launches a Clojure REPL (full Classpath access)make uberjar- create an executable Uberjar of the projectmake run- run/execute the Uberjar artifact
Orchard is a Docker-based sandbox for macOS users. It builds an Ubuntu container with Java 21, Maven, OpenJML, and Fray pre-installed — including native aarch64 (Apple Silicon) support.
./orchard.sh # Enter the orchard interactively
./orchard.sh make check # Run a specific command inside the orchard
The first run builds the Docker image (this takes a few minutes). Subsequent runs reuse the cached image. The container mounts only the project directory at /workspace — no home directory credentials or /var are exposed.
Important: Do git push / git pull outside the orchard, on your host machine.
Bubblewrap is a lightweight, unprivileged tool for constructing sandboxes.
This repo contains a Bash script, bw-opencode, that launches opencode within a Bubblewrap sandbox.
You are not required to use either sandbox utility, but they serve as helpful examples.
Other alternatives include:
- VirtualBox VM / Vagrant
- firejail
- a microVM
- boxlite
- OpenSandbox
There are a number of additional commands, skills, and utilities in this repo to improve the agent-based workflow.
Copy the desired commands and skills into your .opencode or .claude directory. Adjusting naming as needed.
commands - contains common commands you can use directly or adapt for you project
/optimize-code @some/path/to/code- Perform an optimization review of the code/enhance-code @some/path/to/code- Review the code for quality and spec alignment/spec-evidence @some/spec.md- Update the spec.md file so Scenarios link to source and tests. You can also list src and test dirs to focus the command if needed/sample-prompt Some prompt text- Perform verbalized sampling of the given prompt
skills - contains skills for advanced modeling techniques
- For Alloy, the
alloy-moreskill should be preferred - For OpenJML, if the specs are simple don't use a skill. If the specs are challenging, try
openjml-more - For TLA+, if the spec is simple don't use a skill. If the specs are challenging, try
tlaplus-more
The scripts directory contains additional tools/scripts to assist in agent-based development
evidence.shis a doctest tool that turns "living docs" (spec.md) into verification artifacts. Validation + Verification in a single source.
Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in this crate by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.