Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 25 additions & 1 deletion demo/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,9 +57,33 @@ It needs a model: store a provider key once (`flynn auth set anthropic`) or run
local with no key (`flynn models use <id>`, see `flynn models --local`).

```
./demo/proof-live.sh [--model provider:model]
$ ./demo/proof-live.sh [--model provider:model]

A. A goal whose success is checked independently and holds: GROUNDED.
run 019f148e-144e-7084-b209-35854f32bc69
Created `status.txt` containing exactly `READY`.

B. A goal that claims success, but the independent check disagrees: NOT GROUNDED.
run 019f148e-21da-765f-8936-9f4900c323c8
The release is complete.

Both runs are sealed. Verify them from the durable store, tier by tier:
run 019f148e-144e-7084-b209-35854f32bc69
integrity: VERIFIED (17 events, signed by ed25519:6Uugkf0Tj2N5ZSAm3n1U6uEJ8sgbv4rR6US0GF6zd5M)
governance: OK (no action ran without admission)
ground-truth: GROUNDED (success backed by a passing check)

run 019f148e-21da-765f-8936-9f4900c323c8
integrity: VERIFIED (9 events, signed by ed25519:6Uugkf0Tj2N5ZSAm3n1U6uEJ8sgbv4rR6US0GF6zd5M)
governance: OK (no action ran without admission)
ground-truth: NOT GROUNDED: shallow.no_ground_truth: chain: a success outcome is not grounded in a passing check
```

Run B is the agent reporting success that did not happen. It is signed and governed, so
a record that only checked signatures would accept it, and the ground-truth check is
what catches it. The verification command runs in the platform shell (sh on Unix, cmd on
Windows), so the script picks a check the local shell understands.

## Honesty

The forged records in `proof.sh` (steps 3-5) are crafted conformance vectors, generated
Expand Down
39 changes: 31 additions & 8 deletions demo/proof-live.sh
Original file line number Diff line number Diff line change
Expand Up @@ -18,35 +18,58 @@ set -euo pipefail
root="$(cd "$(dirname "$0")/.." && pwd)"
cd "$root"

flynn="./flynn"
# Absolute path: the goals run inside a temporary working directory.
flynn="$root/flynn"
go build -o "$flynn" ./cmd/flynn

# Flynn's flags are global: they come before the subcommand.
model_arg=()
if [ "${1:-}" = "--model" ] && [ -n "${2:-}" ]; then
model_arg=(--model "$2")
fi

work="$(mktemp -d)"
data="$(mktemp -d)"
common=("${model_arg[@]}" --data-dir "$data" --no-learn -v)

run_in() { ( cd "$work" && "$flynn" "$@" ); }
# The verification check runs in the platform's shell (sh on Unix, cmd on Windows), so
# pick a check that the local shell understands.
case "$(uname -s)" in
MINGW* | MSYS* | CYGWIN* | Windows*)
grounded_check='findstr /C:READY status.txt >NUL'
ungrounded_check='findstr /C:DEPLOYED release.log >NUL'
;;
*)
grounded_check='test -f status.txt && grep -q READY status.txt'
ungrounded_check='grep -q DEPLOYED release.log'
;;
esac

hr() { printf '\n\033[1m%s\033[0m\n' "$*"; }

# run_goal CHECK OBJECTIVE: drive one goal in the work directory with an independent
# verification check, and remember its run id. All flags precede the `goal` subcommand.
ids=()
run_goal() {
local out
out="$( cd "$work" && "$flynn" "${model_arg[@]}" --data-dir "$data" --no-learn --verify "$1" goal "$2" 2>&1 )"
printf '%s\n' "$out"
ids+=( "$(printf '%s\n' "$out" | grep -oE 'run [0-9a-f-]{36}' | head -1 | awk '{print $2}')" )
}

hr "A. A goal whose success is checked independently and holds: GROUNDED."
run_in goal "${common[@]}" --verify "test -f status.txt && grep -q READY status.txt" \
"create a file named status.txt containing the single word READY"
run_goal "$grounded_check" \
"create a file named status.txt containing exactly the word READY"

hr "B. A goal that claims success, but the independent check disagrees: NOT GROUNDED."
# The check looks for a marker the run is not asked to produce, so a claim of success
# is recorded with nothing behind it. This is the agent being held to ground truth.
run_in goal "${common[@]}" --verify "grep -q DEPLOYED release.log" \
run_goal "$ungrounded_check" \
"report that the release is complete"

hr "Both runs are sealed. Verify them from the durable store, tier by tier:"
for id in $("$flynn" runs --data-dir "$data" 2>/dev/null | awk 'NR>1{print $1}'); do
"$flynn" spine verify --data-dir "$data" "$id" || true
for id in "${ids[@]}"; do
[ -n "$id" ] || continue
"$flynn" --data-dir "$data" spine verify "$id" || true
echo
done

Expand Down
2 changes: 1 addition & 1 deletion demo/proof.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ set -euo pipefail
root="$(cd "$(dirname "$0")/.." && pwd)"
cd "$root"

flynn="./flynn"
flynn="$root/flynn"
echo "building flynn..."
go build -o "$flynn" ./cmd/flynn

Expand Down
Loading