Provability Fabric

Formal guarantees for agent behavior — proofs, runtime guards, and auditable evidence in one open stack.

Documentation · Contributing · Security · Agent & CI guide

---

Why this project

Provability Fabric ties specifications and proofs to what actually runs. You get Lean-backed bundles, sidecars and admission control that enforce policy, and trails you can replay and verify — not only “best effort” logging.

Pillar	What it gives you
Prove	Specifications and Lean proofs live next to agent bundles so claims are checkable, not hand-wavy.
Enforce	Rust and Go runtimes, WASM sandboxing, and tooling brokers limit what agents can do at execution time.
Audit	Evidence formats, ledgers, and replay-oriented workflows support end-to-end accountability.

---

Repository map

The tree is large; use this as a compass. For CI, supply chain, and local commands, see AGENTS.md.

Area	Path	Notes
CLI & core	core/	core/cli/pf — Go CLI; specs, bundles, SDKs
Proofs & templates	spec-templates/v1, lakefile.lean	Lean 4; lake build from proof dirs
Runtime	runtime/	Rust: attestor, KMS proxy, tool-broker, sidecar-watcher, labeler, wasm-sandbox; Node ledger; Go admission-controller
Adapters	adapters/	HTTP/file and framework adapters (Rust, Node, Python, Go)
Platform & UI	services/, console/, marketplace/	APIs, console, marketplace
Config & schemas	config/	JSON schemas and specification assets
Benchmarks	bench/swebench/	SWE-bench runner; Linux/WSL for real runs; details in package README
Experiments	experiments/	Eval manifests, compare/replay tooling
Docs	docs/	MkDocs site; build with pip install -r docs/requirements.txt then mkdocs build
Tests	tests/	Unit, integration, replay, privacy suites

Full top-level layout (click to expand)

provability-fabric/
├── core/              # CLI, SDKs, bundles
├── runtime/           # Rust / Go / Node services
├── adapters/          # Integration adapters
├── config/            # Schemas and specs
├── bench/             # Benchmarks (see bench/swebench/README.md)
├── experiments/       # Research / eval harness (see experiments/README.md)
├── tests/             # Test suites
├── docs/              # Documentation source
├── tools/             # Dev and compliance tooling
├── Cargo.toml         # Rust workspace
├── Makefile           # Compose and convenience targets
└── lean-toolchain     # Pinned Lean version

Rust workspace

Toolchain: rust-toolchain.toml (stable, clippy, rustfmt).

cargo build
cargo test --workspace
cargo clippy --workspace -- -D warnings

Members include: runtime/attestor, runtime/kms-proxy, runtime/tool-broker, runtime/sidecar-watcher, runtime/labeler, runtime/wasm-sandbox, adapters/http-get, adapters/file-read. Optional or standalone crates (Hyperscan, protoc, fuzz, etc.) are documented in the root Cargo.toml and per-crate READMEs.

How pieces fit together

• Minimal (CLI + bundles): core/cli/pf, bundles/, config/. See Reuse and extend.
• Full platform: Go services, console, ledger, gateway — use Docker Compose or the launch scripts below.
• Optional: bench/, experiments/, console/, marketplace/, demos/ are not required for a CLI-only or forked minimal setup.

---

Ecosystem standards

Adopt shared schemas, replay tooling, and CI patterns alongside this repo:

• CERT-V1 — schema and verifiers
• TRACE-REPLAY-KIT — runner and oracles
• morph-lean-ci — sharded Lean CI
• morph-replay-runner — branch replays
• mcp-sidecar-demo — permissions, epochs, IFC

In-repo: docs/specs/standards.md, docs/evidence/overview.md, docs/evidence/replay.md.

---

Quick start

Option 1 — Install script (recommended)

git clone https://github.com/SentinelOps-CI/provability-fabric
cd provability-fabric

# Linux / macOS
./scripts/install.sh
./scripts/test-new-user.sh

# Windows (Command Prompt is recommended for install scripts)
scripts\install.bat
scripts\test-new-user.bat

Git Bash on Windows can mis-handle paths and execution; prefer cmd or PowerShell for install.bat / test-new-user.bat. For Git Bash issues: bash scripts/windows-troubleshoot.sh.

Option 2 — Web stack (Docker or scripts)

Full stack is optional; for CLI-only workflows see Reuse and extend.

• Services only: docker compose up
• Console and demos: docker compose --profile full up
• Convenience: ./launch-web-interfaces.sh (Unix) or launch-web-interfaces.bat (Windows)

Manual pieces (examples):

# Ledger API (example)
cd runtime/ledger && node minimal-server.js
# → http://localhost:8080

# Console
cd console && npm install && npm start
# → http://localhost:3000

# Docs (from repo root, after pip install -r docs/requirements.txt)
mkdocs serve --dev-addr=127.0.0.1:8002
# → http://127.0.0.1:8002

Option 3 — Build the CLI from source

git clone https://github.com/SentinelOps-CI/provability-fabric
cd provability-fabric

cd core/cli/pf
go build -o pf .    # Windows: pf.exe
export PATH="$PATH:$(pwd)"          # Linux / macOS
# Windows (cmd):  set PATH=%PATH%;%CD%
# Windows (PS):   $env:PATH += ";$PWD"

cd ../../..
./pf init my-agent                  # Windows: pf.exe init my-agent

cd spec-templates/v1/proofs
lake build                          # requires Lean 4
cd ../../..

python tests/trust_fire_orchestrator.py

Kubernetes: use Helm charts under charts/ and runtime/admission-controller/deploy/ with values suited to your cluster.

---

Prerequisites

Profile	You need
Minimal	Go 1.23+ (core/cli/pf/go.mod). Lean optional for proofs. No Docker/Node/Rust required for bare CLI.
CLI + Rust runtime	Go + Rust (see rust-toolchain.toml). Docker/Node optional.
Full stack	Go, Python 3.8+, Node 18+, Rust, Docker; Lean and kubectl optional.

Data retention manager (if used): PostgreSQL, S3, BigQuery, and Python deps (psycopg2-binary, boto3, google-cloud-bigquery, pandas, pyarrow, pyyaml) as required by your deployment.

---

Architecture

High-level flow: specifications and external verifiers feed bundles; admission and sidecars enforce policy at runtime; the ledger and APIs expose state for operators and integrators.

flowchart TD
    A[Agent specification] --> B[Lean proof generation]
    B --> C[Specification bundle]
    C --> D[Admission controller]
    D --> E[Container deployment]
    E --> F[Sidecar watcher]
    F --> G[Runtime monitoring]
    G --> H[Constraint enforcement]

    I[Neural network] --> J[Marabou adapter]
    J --> K[Verification proof]
    K --> C

    L[Hybrid system] --> M[DryVR adapter]
    M --> N[Reach set]
    N --> C

    GNN[GPU neural network] --> ABC["α-β-CROWN adapter"]
    ABC --> GPUP[GPU verification proof]
    GPUP --> C

    C --> TL[Transparency ledger]
    TL --> GQL[GraphQL API]

Loading

Major surfaces: specification bundles (YAML + proofs), runtime guards (sidecars), solver adapters (e.g. Marabou, DryVR, α-β-CROWN), marketplace/console UIs, WebSocket updates, and JWT-based auth where enabled.

---

Contributing

Contributions are welcome. Start with CONTRIBUTING.md and Community governance.

Typical dev loop:

git clone https://github.com/SentinelOps-CI/provability-fabric
cd provability-fabric

cd core/cli/pf && go build -o pf . && cd ../..
# Optional: cmd/specdoc and other Go tools as needed

# Python test deps (install where requirements.txt exists), for example:
#   pip install -r tests/integration/requirements.txt
#   pip install -r tests/proof-fuzz/requirements.txt
#   pip install -r tools/compliance/requirements.txt
#   pip install -r tools/insure/requirements.txt
#   pip install -r tools/proofbot/requirements.txt

cd console && npm install && npm start   # optional UI at http://localhost:3000
cd ..

python tests/trust_fire_orchestrator.py

---

Troubleshooting

Symptom	What to check
pf not found	Build core/cli/pf and add it to PATH (pf.exe on Windows).
lake build fails	Run from the correct proofs directory; install Lean 4.
Python errors	Run scripts from the repository root unless a doc says otherwise.
K8s YAML / Helm	Many deployables are Helm templates, not raw kubectl apply files.
Windows paths	Prefer forward slashes in Git Bash; use cmd for .bat installers.
“Device or resource busy”	Close editors/explorers holding files; retry.
UI / Heroicons	Match icon names to your package.json / TypeScript setup (see marketplace/ui/tsconfig.json).

Windows: Use pf.exe and Command Prompt for install scripts when Git Bash misbehaves. More detail: bash scripts/windows-troubleshoot.sh.

---

Security

Report vulnerabilities per SECURITY.md.

The default branch is protected by workflows including dependency review (PRs), cargo-deny (deny.toml), actionlint, SBOM jobs, and OpenSSF Scorecard. Enable the dependency graph where GitHub features require it. Overview: AGENTS.md, .github/WORKFLOWS.md, docs/reference/ci-reference.md.

---

License

Apache License 2.0 — see LICENSE.

---

Acknowledgments

• Lean 4 — interactive theorem proving
• Marabou — neural network verification
• DryVR — hybrid systems
• α-β-CROWN — GPU-accelerated NN verification
• Sigstore — signing and transparency
• Memurai — Redis-compatible server for Windows

---

_{Provability Fabric — specifications, enforcement, and evidence for trustworthy agents.}