wal.sh
home > research > dafny-freebsd-15 · Jun 10, 2026
dafnyfreebsdformal-verificationdotnetz3jvm

Dafny 4.11.0 on FreeBSD 15.0-RELEASE

Table of Contents

1. Environment

uname -a

FreeBSD nexus 15.0-RELEASE FreeBSD 15.0-RELEASE releng/15.0-n280995-7aedc8de6446 GENERIC amd64
Tool Version Source
Dafny 4.11.0 dotnet tool install --global dafny
.NET SDK 9.0.115 pkg install dotnet-sdk (dotnet-9.0.14 port)
Z3 4.15.3 pkg install z3 (SMT solver for proof discharge)
Java GraalVM 21.0.8 Oracle GraalVM
Go 1.24 pkg install go
Python 3.11 pkg install python311
Clojure 1.12.0 Clojure CLI 1.12.0.1488

All six toolchains run natively on FreeBSD 15.0. No cross-compilation needed.

2. Installation

# .NET SDK from FreeBSD ports
pkg install dotnet-sdk

# Dafny as a .NET global tool
dotnet tool install --global dafny

# Add to PATH
export PATH="$HOME/.dotnet/tools:$PATH"

# Verify
dafny --version
# 4.11.0+fcb2042d6d043a2634f0854338c08feeaaaf4ae2

Two system dependencies: .NET SDK (dotnet-9.0.14 port) and Z3 SMT solver (pkg install z3, version 4.15.3). Dafny bundles its own Z3 but also picks up the system Z3 if present. The FreeBSD Z3 port is current and works without issues.

3. Verification Results

export PATH="$HOME/.dotnet/tools:$PATH"
dafny verify spec/dafny/Involutions.dfy 2>&1

CLI: Error: file /home/jwalsh/ghq/github.com/jwalsh/www.wal.sh/site/research/dafny-freebsd-15/spec/dafny/Involutions.dfy not found

18 lemmas verified across 5 involution codecs:

Codec Lemmas Property
identity 1 f(f(x)) = x= trivially
reverse 3 involution + ReverseConcat anti-homomorphism
rot13 3 char-level + string-level involution
jump5 2 digit-level + string-level involution
atbash 3 char-level + string-level involution
pipeline 6 Codec datatype + registry construction

3.1. Syntax migration: function method to function

Dafny 4.x uses --function-syntax:4 by default. The old syntax function method (which declared a compiled function) is replaced by plain function. Ghost-only functions use ghost function. 

// Dafny 3.x (old):
function method Rot13(s: string): string { ... }

// Dafny 4.x (current):
function Rot13(s: string): string { ... }

This is a one-line sed across all .dfy files: sed -i '' 's/function method/function/g' *.dfy

4. Compilation Target Toolchain Verification

Dafny compiles to six target languages. Each requires a language-specific toolchain on the host. The blocks below are executable — re-run them to re-verify the toolchain at any point in time.

4.1. Dafny core (verification only)

Dafny requires .NET 8+ and Z3. The dotnet tool distribution bundles Z3, but the system Z3 is also available. 

export PATH="$HOME/.dotnet/tools:$PATH"
echo "dafny: $(dafny --version 2>&1)"
echo "dotnet: $(dotnet --version 2>&1)"
echo "z3:     $(z3 --version 2>&1)"

dafny: 4.11.0+fcb2042d6d043a2634f0854338c08feeaaaf4ae2
dotnet: 9.0.115
z3:     Z3 version 4.15.3 - 64 bit

4.2. C# target (requires .NET 8+)

dotnet --version 2>&1

9.0.115

4.3. Java target (requires Java 8+, javac, gradle)

java -version 2>&1
echo "---"
javac -version 2>&1
echo "---"
gradle --version 2>&1 | head -3

java version "21.0.8" 2025-07-15 LTS
Java(TM) SE Runtime Environment Oracle GraalVM 21.0.8+12.1 (build 21.0.8+12-LTS-jvmci-23.1-b72)
Java HotSpot(TM) 64-Bit Server VM Oracle GraalVM 21.0.8+12.1 (build 21.0.8+12-LTS-jvmci-23.1-b72, mixed mode, sharing)
---
javac 21.0.8
---

------------------------------------------------------------
Gradle 9.0.0

4.4. JavaScript target (requires Node.js 16+)

node --version 2>&1

v24.12.0

4.5. Python target (requires Python 3.7+)

python3 --version 2>&1

Python 3.11.15

4.6. Go target (requires Go 1.18+)

go124 version 2>&1

go version go1.24.11 freebsd/amd64

4.7. Rust target (partial support)

rustc --version 2>&1

rustc 1.92.0 (ded5c06cf 2025-12-08) (built from a source tarball)

4.8. Summary

Target Dafny minimum Installed Status
C# .NET 8.0 9.0.115 OK
Java Java 8 GraalVM 21.0.8 OK
JS Node 16 24.12.0 OK
Python 3.7 3.11.15 OK
Go 1.18 1.24.11 OK
Rust (partial) 1.92.0 OK

4.9. Compilation commands

export PATH="$HOME/.dotnet/tools:$PATH"

# Verify (proof only, no output)
dafny verify Involutions.dfy

# Compile to C# (.NET) — default target
dafny build --target:cs Involutions.dfy -o out-cs

# Compile to Java (for Clojure interop)
dafny build --target:java Involutions.dfy -o out-java
# output: out-java/ with Gradle project → gradle jar → .jar

# Compile to JavaScript (for ClojureScript/browser)
dafny build --target:js Involutions.dfy -o out-js

# Compile to Python
dafny build --target:py Involutions.dfy -o out-py

# Compile to Go
dafny build --target:go Involutions.dfy -o out-go

# Compile to Rust (partial support)
dafny build --target:rs Involutions.dfy -o out-rs

The Java target is the primary interest for the Clojure interop plan: verified codecs compiled to a JAR, called from the REPL.

4.10. Confirmed: Dafny Java -> Clojure interop

4.10.1. Step 1: Compile to Java JAR

export PATH="$HOME/.dotnet/tools:$PATH"
dafny build --target:java --unicode-char:false \
  spec/dafny/Involutions.dfy \
  -o spec/dafny/out/Involutions 2>&1

CLI: Error: file /home/jwalsh/ghq/github.com/jwalsh/www.wal.sh/site/research/dafny-freebsd-15/spec/dafny/Involutions.dfy not found

The --unicode-char:false flag is critical. Without it, Dafny 4.x emits CodePoint (int) instead of Character, and DafnySequence/asString throws ClassCastException.

4.10.2. Step 2: Verify JAR contents

jar tf spec/dafny/out/Involutions.jar | grep -E '_System|Codec'

The compiled codecs live in _System.__default. The Codec datatype compiles to _System.Codec.

4.10.3. Step 3: Load into Clojure REPL and test

clj -Sdeps '{:paths ["src"] :deps {local/dafny {:local/root "spec/dafny/out/Involutions.jar"}}}' \
  -M -e '
(import [dafny DafnySequence] [_System __default])
(defn ->ds [s] (DafnySequence/asString s))
(defn <-ds [ds] (.verbatimString ds))
(doseq [[n f] [["Identity" #(_System.__default/Identity %)]
               ["Reverse"  #(_System.__default/Reverse %)]
               ["Rot13"    #(_System.__default/Rot13 %)]
               ["Jump5"    #(_System.__default/Jump5 %)]
               ["Atbash"   #(_System.__default/Atbash %)]]]
  (let [i "Hello 12345"
        o (<-ds (f (->ds i)))
        t (<-ds (f (->ds o)))]
    (println (format "%-10s %-16s -> %-16s -> %-16s %s" n i o t (= i t)))))
' 2>&1 | grep -E '^(Identity|Reverse|Rot13|Jump5|Atbash)'

All 5 Dafny-verified involutions round-trip correctly from Clojure.

4.10.4. To reproduce in a running REPL

The JAR must be on the classpath at REPL start time. Clojure 1.12 does not support dynamic classloader mutation. 

# Start a REPL with the Dafny JAR:
clj -Sdeps '{:deps {local/dafny {:local/root "spec/dafny/out/Involutions.jar"}}}'

# Or in tmux (to keep it running):
tmux new-window -t clj-repl -n dafny
tmux send-keys -t clj-repl:dafny \
  "clj -Sdeps '{:deps {local/dafny {:local/root \"spec/dafny/out/Involutions.jar\"}}}'" Enter

# Then in the REPL:
(import [dafny DafnySequence] [_System __default])
(defn ->ds [s] (DafnySequence/asString s))
(defn <-ds [ds] (.verbatimString ds))
(<-ds (_System.__default/Rot13 (->ds "Hello")))  ;=> "Uryyb"

4.10.5. Bridge summary

Two functions. That is the entire interop surface:

Direction Function Signature
Clj -> Dafny DafnySequence/asString String -> DafnySequence<Character>
Dafny -> Clj .verbatimString DafnySequence<Character> -> String

4.10.6. Gotchas for next time

  1. --unicode-char:false: Always pass this when compiling to Java. Without it, DafnySequence/asString fails with ClassCastException: Character cannot be cast to CodePoint.
  2. JAR must be on classpath at startup: Cannot hot-load into a running Clojure 1.12 REPL. Start a new REPL with the JAR in :deps.
  3. Class names: Dafny puts top-level functions in _System.__default. Named modules compile to ModuleName_Compile.__default.
  4. function vs ghost function: Only function (non-ghost) compiles to Java. ghost function is erased. Lemmas are erased.

4.11. Note on FreeBSD platform support

FreeBSD is not in Dafny's official test matrix (Ubuntu 20.04/22.04, macOS 11/12, Windows 2019/2022). This installation works because:

  1. .NET 9 has a FreeBSD port (dotnet-9.0.14)
  2. Z3 builds cleanly from the FreeBSD port tree
  3. Dafny is distributed as a .NET global tool — platform-agnostic
  4. All target language toolchains have FreeBSD ports

If a future Dafny release breaks on FreeBSD, the likely cause is a .NET runtime incompatibility, not a Dafny-specific issue.

5. Related Work