PathFence: A Lean 4 Path Checker—and Where Its Guarantees Stop

Correction (2026-10-28). The earlier version of this article described a Workspace API, Windows support, a macOS/BSD fallback, a pure-Python package for Python 3.9+, four explicit openat2 resolve flags, a formal/ directory, a count of 15 theorems and five theorem names, none of which exist, and unsupported microsecond benchmarks. Those claims did not match the repository. This article replaces them with a description checked against code commit e697b4a, with the README packaging clarification in 06753e0. Thanks to the reporter of issue #2. I am responsible for correcting the article published on my account.

PathFence is a Lean 4 library and command-line tool for lexical path-policy decisions. It is not a sandbox or a complete verified file-system implementation.

Repository: https://github.com/hiroki-abe-58/pathfence

What the checker does

A policy has a base directory, allowed roots and denied roots. Roots must already be canonical; /w/.. is refused rather than silently normalized. Requests return allow, deny, or reject.

$ pathfence check --allow /tmp/allowed_dir -- /tmp/allowed_dir_malicious/secret ../x a/../b
{"input":"/tmp/allowed_dir_malicious/secret","decision":"deny","path":"/tmp/allowed_dir_malicious/secret"}
{"input":"../x","decision":"reject","reason":"escapes"}
{"input":"a/../b","decision":"allow","path":"/tmp/allowed_dir/b","root":"/tmp/allowed_dir","rel":"b"}

Empty input and input containing NUL are rejected. Absolute paths are normalized lexically. Relative paths are walked beneath the base: a .. that would leave it is rejected even if later segments would return inside. Containment compares complete segments, so /tmp/ab is not inside /tmp/a. An allowed result names both the allowed root and the relative remainder rel.

These are POSIX lexical rules, not native Windows path rules. Symlinks, mounts, hard links, case folding and concurrent file-system changes are outside the checker’s view.

What Lean proves

The main theorem, check_allow_iff, characterizes exactly when the modeled checker allows a resolved path: it resolves successfully, lies within an allowed root, and lies within no denied root. Other published statements include:

• resolve_rel_spec: successful relative resolution agrees with the specified beneath walk.
• resolve_rel_within: successful relative resolution remains within the base.
• allowedUnder_spec: the reported root is allowed and its remainder reconstructs the resolved path.
• parseRoot_render: a root string that parses successfully renders back to exactly that string.
• within_iff_render: for a root other than /, segment containment corresponds to equality or a prefix followed by /.

The repository pins 25 published statements. The audit reports 147 theorem declarations, including helpers and generated equation lemmas, at the code revision above. This is not a claim of 147 separate security guarantees. The audit checks dependencies on Lean’s standard axioms, replays library modules through the kernel checker, and pins the published statements and their transitive library definitions by SHA-256. The library imports only Lean’s Init.

The audit itself remains a trust boundary: someone who changes its inputs or implementation can change what it checks. The CLI’s argument parsing, UTF-8 handling and JSON output, the compiler/runtime, Python examples and operating system are not covered by a complete end-to-end proof.

Tests complement the proof

The suite compares the CLI against an independent Python implementation of the documented rules and uses posixpath.normpath for absolute inputs. On Linux it also compares 1,500 generated relative paths against real openat2(RESOLVE_BENEATH | RESOLVE_NO_SYMLINKS) calls on a directory tree without symlinks. Agreement on that tested domain is evidence, not a proof of equivalence to the kernel.

The mutation check plants 11 bugs in the CLI and requires the suite to detect them; three further mutations target the extraction example. GitHub Actions runs build, audit, tests and mutation checks. Tests and review in separate Claude sessions have found issues both around the proven function and in the intended specification, including invalid UTF-8 handling, option-like path arguments, empty inputs and noncanonical roots.

File access still needs kernel enforcement

Do not take an allowed path and assume an ordinary open(path) is safe. A path can be lexically allowed while traversing a symlink into a denied directory.

The repository’s example examples/safe_open.py combines the checker with Linux openat2, opening rel beneath a handle for root. Its signature is:

safe_open(path, allow, deny=(), base=None, flags=os.O_RDONLY, mode=0o644)

This is not a pathfence.Workspace API. The example explicitly passes RESOLVE_BENEATH | RESOLVE_NO_SYMLINKS. Linux’s RESOLVE_NO_SYMLINKS also implies no magic-link traversal; that does not mean the code explicitly passes four flags. The example requires Linux 5.6+ and has no macOS/BSD fallback or native Windows implementation. Trusted root selection and file-system assumptions still matter.

The newer examples/safe_extract.py handles tar/zip archives, accepts only regular files and directories, checks member names, and creates members beneath a new private destination with exclusive creation. It additionally uses RESOLVE_NO_XDEV. Archive links are rejected. Its runtime checks and kernel behavior are separate from the Lean proofs about names; it is not a formally verified archive parser.

There is no Workspace, subworkspace, or atomic_write lifecycle API in this revision. The former article’s microsecond openat2 and fallback benchmarks were unsupported and have been removed. The repository’s actual benchmark concerns the lexical CLI, not those fictional APIs.

Try it

The published pathfence 0.1.0 package is on PyPI and requires Python 3.10+. The 0.1.0 wheels were built from tag v0.1.0 (a959fdc), not from the newer code revision discussed above. They bundle the Lean executable; this is not a pure-Python implementation.

python -m pip install --only-binary=:all: pathfence
pathfence check --allow /tmp/allowed_dir -- ../x a/../b

For the source and verification workflow:

git clone https://github.com/hiroki-abe-58/pathfence
cd pathfence
./scripts/reproduce.sh

The reproduction workflow needs git, elan, Python, sha256sum and Linux 5.6+ for the kernel tests. Its openat2 calls must not be blocked by seccomp; the workflow fails if any test is skipped. Consult the README for current platform support and prerequisites. Package installation alone does not make an agent’s file tools confined.

PathFence is Apache-2.0 licensed and experimental. I started and lead the project; code and proofs were developed with Claude Code (Claude Opus 5.5) and reviewed only by AI, in separate Claude sessions; no human has reviewed them yet. Human review, counterexamples and reproducible issues are welcome.