Dafnyutils is a benchmark repository that tests whether agents can write code and proofs from formal specifications of GNU coreutils written in Dafny. It includes a model of system state as well as program logic. This model lets us specify and verify effects on the system. We check the model through differential testing: we compare its behavior with the original GNU coreutils binaries.
Read CONTRIBUTING.md for the contribution process and required PR evidence. Use these four guides for detailed tasks:
| Your task | Guide |
|---|---|
| Add a utility from setup through review | Add a utility |
| Understand shared contracts and what the proof assumes | Use the core API |
| Run generated cases and reproduce mismatches | Use the fuzzer |
| Port upstream GNU scenarios into utility Python tests | Add test cases |
Follow repository instructions, bench rules and Dafny style.
Install these tools on your host before you start:
- Git.
- Docker, with the Docker engine running.
- VS Code with the Dev Containers extension, or the Dev Container CLI for terminal use.
Use the development container included in this repository. The container has been tested on Linux x86-64 (Ubuntu 24.04). Other architectures have not been tested.
We use a version of Dafny changed for dafnyutils. Its source is pinned in the
dafny/ submodule from git@github.com:prosyslab/dafny.git (expecto branch).
You must use the Dafny built inside the development container, available
at /usr/bin/dafny-benchmark in the container.
In VS Code, open this checkout and select Dev Containers: Reopen in Container. Wait for setup to finish.
For terminal use, run:
# On the host, from this repository's root:
devcontainer up --workspace-folder .Expected final output (after build/setup logs; IDs vary):
{"outcome":"success","containerId":"<container-id>","remoteUser":"vscode","remoteWorkspaceFolder":"/workspace/dafnyutils"}
devcontainer exec --workspace-folder . zshExpected result: an interactive shell in the container. The prompt style varies:
<container prompt> /workspace/dafnyutils $
The CLI uses the same configuration and setup script as VS Code.
The container name is <USER>-dafnyutils, where <USER> is the value of USER
on your host. For example, if USER is duncan, the name is duncan-dafnyutils.
Inside the container, the repository is /workspace/dafnyutils.
Setup installs Python 3.12, .NET 8, Rust, Z3, tmux and native build tools. Budget 10–30 minutes for initial downloads and compilation. A clean Linux x86-64 setup used up to about 10 GiB of memory, excluding the image build.
Run repository commands inside the container to check environment setup:
cd /workspace/dafnyutils
source .venv/bin/activate
make check-environmentExpected output:
Checking: python3 --version
Python 3.12.<patch>
...
No broken requirements found.
...
Checking: tmux -V
tmux <version>
...
Dafny program verifier finished with 4 verified, 0 errors
Environment ready. The StreamCopy result checks the verifier, not a utility proof.
make check-environment checks Python dependencies, Docker/Compose access, Rust,
Z3, tmux and the bundled dafny-benchmark. It verifies the StreamCopy client. Success ends with
Environment ready and a verifier result of 4 verified, 0 errors. This checks
the tools. Setup runs the same check automatically.
dafnyutils/
├── .devcontainer/ # Development container and setup scripts
├── .githooks/ # Repository Git hooks
├── .github/ # CI workflows and pull request template
├── .vscode/ # VS Code and Dafny extension settings
├── bench/ # Benchmark definitions and Dafny sources
│ ├── algorithm/ # Algorithm tasks
│ ├── core/ # Shared system models, IO contracts and native adapters
│ └── utils/ # GNU coreutils task specifications, implementations and proofs
├── coreutils/ # Pinned upstream GNU coreutils submodule
├── dafny/ # Pinned Dafny submodule customized for this project
├── docker/ # Task and evaluation container build definitions
├── docs/ # Contributor guides and API documentation
├── example/ # Worked examples
│ └── copy/ # Stream-copy specification, implementation and proof
├── src/ # Python authoring, verification and evaluation tooling
│ ├── analysis/ # Evaluation result analysis
│ ├── benchmarks/ # Task discovery, scaffolding, builds and validation
│ ├── evaluation/ # Evaluation environments, task preparation and scoring
│ └── runtime/ # Runtime support for evaluation
├── tools/ # Build scripts and repository maintenance tools
│ ├── benchmark_templates/ # Templates for new utility and algorithm tasks
│ └── coreutils_fuzzer/ # Generated-input comparison with GNU coreutils
└── _build/ # Generated build artifacts
This example copies standard input to standard output. It shows the same
Spec → Core → Proof → entry structure as a utility contribution, with only two
IO calls. The complete files are in
example/copy/.
Use the development container. Run the commands below
from /workspace/dafnyutils with .venv/bin on PATH.
Write down the behavior before implementing it:
- Read finite bytes from standard input, including NUL and non-UTF-8 bytes.
- Write the bytes that were read, even if the read ended with an error.
- Return exit status 0 only if both reading and writing succeed; otherwise return 1.
- A failed write may leave a prefix of the requested bytes on standard output.
- Do not write diagnostics or change files.
The example has no options or file operands. It is a teaching program, not a
GNU cat contribution. A real utility also needs its approved option, diagnostic
and error behavior, GNU comparison tests and generated fuzz cases.
Open CopySpec.dfy.
CopyResult describes the input consumed and output written using the existing
contracts in bench/core/IOContract.dfy:
twostate predicate CopyResult(io: BenchIO.IO, readErr: int, writeErr: int)
reads io.stdinRegion, io.stdoutRegion, io.trustedStreamsRegion
{
exists data: BenchWorld.Bytes, committed: nat ::
C.ReadStdinWithOutcomeSpec(
old(io.stdin()), old(io.trustedStreams()), io.stdin(), data, readErr) &&
C.WriteStdoutWithOutcomeSpec(
old(io.stdout()), old(io.trustedStreams()), io.stdout(), data, committed, writeErr)
}The same data connects the two contracts. The read contract says it is the
consumed input prefix. The write contract says that exactly committed bytes
from its beginning were appended to stdout. Both contracts include the observed
error code. exists states that these values describe the result; it does not
run an algorithm or choose a different IO result.
old(...) refers to the state before the call. reads lists the state this
predicate uses, including the IO results supplied by the shared library.
twostate allows the predicate to compare the state before and after a call.
The main Spec adds the exit policy and makes the successful result explicit:
twostate predicate Spec(io: BenchIO.IO, exit: int)
reads io.stdinRegion, io.stdoutRegion, io.trustedStreamsRegion
{
(exists readErr: int, writeErr: int ::
CopyResult(io, readErr, writeErr) &&
exit == (if readErr == 0 && writeErr == 0 then 0 else 1)) &&
(exit == 0 ==>
io.stdin() == [] && io.stdout() == old(io.stdout()) + old(io.stdin()))
}On success, input is consumed and its bytes are appended unchanged. On failure,
CopyResult still constrains the consumed and written prefixes. The specification
does not assume that IO succeeds.
CopyCore.dfy contains the code:
method CopyInput(io: BenchIO.IO) returns (readErr: int, writeErr: int)
modifies io.stdinRegion, io.stdoutRegion
ensures CopySpec.CopyResult(io, readErr, writeErr)
{
var data;
data, readErr := io.ReadStdinWithOutcome();
var committed;
committed, writeErr := io.WriteStdoutWithOutcome(data);
}modifies permits changes only to the two stream regions. There is no extra
assertion saying stderr or the filesystem stays unchanged: the narrow list
already guarantees that. The method promises CopyResult for every returned
result, including read and write failures.
CopyProof.dfy proves that
CopyResult, together with the chosen exit status, implies Spec. Its lemma
body is empty because Dafny can prove this small implication from the library
contracts. An empty lemma body is still checked; it is not an assumed fact.
Copy.dfy combines the pieces:
method RunCore(io: BenchIO.IO) returns (exit: int)
modifies io.stdinRegion, io.stdoutRegion
ensures CopySpec.Spec(io, exit)
{
var readErr, writeErr := CopyCore.CopyInput(io);
exit := if readErr == 0 && writeErr == 0 then 0 else 1;
CopyProof.CopyResultImpliesSpec(io, readErr, writeErr, exit);
}The entry method itself promises Spec. The lemma helps prove that promise.
The Spec file imports no implementation or proof file.
CopyCli.dfy gets the process IO
handle with BenchIO.Process(), calls RunCore and passes its result to
BenchIO.Exit. The build uses the existing bench/core/IOExtern.cs adapter
to connect the Dafny calls to real process streams.
make -C example/copy verifyExpected output, exit 0 (the library warnings and make command lines are omitted):
...
Dafny program verifier finished with 10 verified, 0 errors
...
The target uses --verify-included-files to check all five Copy*.dfy files.
It uses the repository's --library setting for bench/core: those existing
contracts are assumptions of this example, not newly proved native IO code.
Dafny warns that these are source-library files. The target allows those warnings,
as the repository's utility verifier does. It does not skip any example proof.
The Dafny methods have no loops or recursion and prove termination of their own code. Actual stream reads can wait for input; completion depends on the supplied IO contracts and a finite input that reaches EOF or an error.
make -C example/copy buildExpected output, exit 0 (other build lines omitted):
...
Dafny program verifier did not attempt verification
...
This creates _build/tutorial-copy/copy.dll. Build and verification are separate
steps, so a successful build does not replace step 5.
printf 'hello\n' | dotnet _build/tutorial-copy/copy.dllExpected output, exit 0:
hello
make -C example/copy testExpected output, exit 0 (build lines omitted):
...
4 passed in <seconds>s
...
Tests.py checks empty input, all 256
byte values, a write to /dev/full, and a directory supplied as stdin. Tests
check stdout, stderr and exit status where applicable. The two error tests must
return 1, not silently report success. These Linux tests exercise the actual
adapter; they do not inject every possible partial read or write failure. The
proof constrains those partial results under the shared IO contracts.
For a exercise, change the exit assignment in Copy.dfy to:
exit := 0;This bug reports success even when reading or writing fails.
make -C example/copy verifyExpected output, exit 2 from make (other lines omitted):
...
Dafny program verifier finished with 9 verified, 1 error
...
The failing condition is the lemma's requirement that the exit status matches the two error results. Now check the executable too:
make -C example/copy testExpected output, exit 2 from make (build output and failure details omitted):
...
2 failed, 2 passed in <seconds>s
...
The two failure cases catch the wrong exit status; the two successful IO cases still pass. Restore the original assignment before continuing:
exit := if readErr == 0 && writeErr == 0 then 0 else 1;make -C example/copy verify testExpected output, exit 0 (other lines omitted):
...
Dafny program verifier finished with 10 verified, 0 errors
...
4 passed in <seconds>s
...