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
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"kind": "CIJobResultBodyClaim",
"schemaVersion": "1",
"jobKey": "provekit/ci/go",
"blastRadiusCid": "blake3-512:3bc39a0377fbd0cef8da644fb97fd6b48f6f3468c8bee8ca7b94f45ff2e6aacaa3fcad1b3d5e2b3a7fff297cb4bcc3bdaf0e7d9bf733da42c591f405021f205b",
"result": "pass",
"outputCid": "blake3-512:080a98e5159b006e57e5cf32250acf7af126224a697154480f869792fe9ea9ebc1012773f66b887302af900ba599696f02165f4a0df1bb30b8d1e287b79b8bfe",
"logCid": "blake3-512:6f83b93d1d7e7d94db4b551e174b1da7ffbf06da906c4ad1f857f4e060b0b96a8cb4deeeeb77c49dfb8a49a45adb1ab7a1963916ab74fe59af6a498c1c168771",
"startedAt": "2026-05-07T00:00:00Z",
"finishedAt": "2026-05-07T00:00:00Z",
"runnerIdentityCid": "blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b",
"policyCid": "blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"inputCids": [
"blake3-512:080a98e5159b006e57e5cf32250acf7af126224a697154480f869792fe9ea9ebc1012773f66b887302af900ba599696f02165f4a0df1bb30b8d1e287b79b8bfe",
"blake3-512:3bc39a0377fbd0cef8da644fb97fd6b48f6f3468c8bee8ca7b94f45ff2e6aacaa3fcad1b3d5e2b3a7fff297cb4bcc3bdaf0e7d9bf733da42c591f405021f205b",
"blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"blake3-512:6f83b93d1d7e7d94db4b551e174b1da7ffbf06da906c4ad1f857f4e060b0b96a8cb4deeeeb77c49dfb8a49a45adb1ab7a1963916ab74fe59af6a498c1c168771",
"blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b"
],
"producer": {
"kind": "ci-runner",
"name": "provekit-ci",
"version": "checked-in"
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"kind": "CIJobResultBodyClaim",
"schemaVersion": "1",
"jobKey": "provekit/ci/java",
"blastRadiusCid": "blake3-512:d647ecccb0831c607db377b7e096eb78e7b39dcbe4b1a44cc633c946d9605afb6bf56597cf266e41ec344a7bfc662f7c6d1ed790e05d3945beabe06da9b75298",
"result": "pass",
"outputCid": "blake3-512:f4419779456b1537f883702a7ca679bf8bf6d98e7ab4157f087436d04c746c5d14759b3b67c305f7d100569bc73a809aa03fe24209877f103d9887ea9886edf3",
"logCid": "blake3-512:52a3b4cebf82f12a4f7df06ea6f8b95d1d87f0b39f4f3be2eee23e23ea023a5592407c5b6f400ab00ba0946e7daafdca0fc69475ac0970508179a3fd467dcb14",
"startedAt": "2026-05-07T00:00:00Z",
"finishedAt": "2026-05-07T00:00:00Z",
"runnerIdentityCid": "blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b",
"policyCid": "blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"inputCids": [
"blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"blake3-512:52a3b4cebf82f12a4f7df06ea6f8b95d1d87f0b39f4f3be2eee23e23ea023a5592407c5b6f400ab00ba0946e7daafdca0fc69475ac0970508179a3fd467dcb14",
"blake3-512:d647ecccb0831c607db377b7e096eb78e7b39dcbe4b1a44cc633c946d9605afb6bf56597cf266e41ec344a7bfc662f7c6d1ed790e05d3945beabe06da9b75298",
"blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b",
"blake3-512:f4419779456b1537f883702a7ca679bf8bf6d98e7ab4157f087436d04c746c5d14759b3b67c305f7d100569bc73a809aa03fe24209877f103d9887ea9886edf3"
],
"producer": {
"kind": "ci-runner",
"name": "provekit-ci",
"version": "checked-in"
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"kind": "CIJobResultBodyClaim",
"schemaVersion": "1",
"jobKey": "provekit/ci/rust",
"blastRadiusCid": "blake3-512:b9698db898dc694764d694835837b9d1266eaf0d63c72a667aba21478d333d61ef140f3152b21692c0e2db7a7a3b03e7e90d4cd84c6aa7bc4d71a29af2cd7a74",
"result": "pass",
"outputCid": "blake3-512:cf85ec708d2cfe4a73ecbd20b3188921a6526b66b13378efa3c7908edcfbc85c1e43266aac8015b440855f1ba6cb6509125639683407e136b4dc41c9d9cbdcab",
"logCid": "blake3-512:a27eeec12607aa5939b00718f6d395fef2e92ce90335bb16922a06fc3dd435aa058430092cff035c0e8b3153157496418c191d389e10458252a974f07b7572c7",
"startedAt": "2026-05-07T00:00:00Z",
"finishedAt": "2026-05-07T00:00:00Z",
"runnerIdentityCid": "blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b",
"policyCid": "blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"inputCids": [
"blake3-512:430f7ae604144abb9810c0ee83dedce757cd12ce1bb3457051c7c94fcccfc237ccb7a909fe471290367bf9649129bdb76d63a392e28f59dad74b5417612e5668",
"blake3-512:a27eeec12607aa5939b00718f6d395fef2e92ce90335bb16922a06fc3dd435aa058430092cff035c0e8b3153157496418c191d389e10458252a974f07b7572c7",
"blake3-512:b9698db898dc694764d694835837b9d1266eaf0d63c72a667aba21478d333d61ef140f3152b21692c0e2db7a7a3b03e7e90d4cd84c6aa7bc4d71a29af2cd7a74",
"blake3-512:cf85ec708d2cfe4a73ecbd20b3188921a6526b66b13378efa3c7908edcfbc85c1e43266aac8015b440855f1ba6cb6509125639683407e136b4dc41c9d9cbdcab",
"blake3-512:ea57d5bb564e290c3cd6fa3e5355e411d279c37be83cd4085d856b6c1210ce27ea65012d9810b1d343aeddd9ddfffd4542991107a3c7cc5121447ac4722ccd4b"
],
"producer": {
"kind": "ci-runner",
"name": "provekit-ci",
"version": "checked-in"
}
}
7 changes: 7 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ help:
@echo " make ci full gate (conformance + test-all) [Linux/CI: 10 peer langs]"
@echo " make conformance catalog + protocol + 11 mint CIDs + self-contract tests"
@echo " make all-mint 11 mint commands (Swift excluded: macOS-only, use mint-swift)"
@echo " make bug-zoo replay executable bug specimens through source-routed CLI"
@echo " make bootstrap-self-contracts"
@echo " re-sign attestations from live kit artifacts"
@echo " override: CONFORMANCE_PROFILE=all CONFORMANCE_JOBS=8"
Expand Down Expand Up @@ -532,6 +533,12 @@ test-rust:
cargo test --release --manifest-path tools/recompute-spec-cids/Cargo.toml
cargo test --release --manifest-path tools/foundation-keygen/Cargo.toml

.PHONY: bug-zoo
bug-zoo:
@echo "=== Bug Zoo: live ProvekIt receipts ==="
env -u PROVEKIT_CLI -u PROVEKIT_BUG_ZOO_EXTERNAL_CLI \
cargo run --manifest-path bug-zoo/Cargo.toml -- --all

.PHONY: test-go
test-go:
cd implementations/go/provekit-ir-symbolic && go test ./...
Expand Down
41 changes: 25 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ accountable edges the rest of the graph must satisfy.
| | |
| --- | --- |
| **Use the CLI** | [docs/quickstart-end-user.md](docs/quickstart-end-user.md) to install and run `provekit`; [docs/reference/protocol-extensions.md#tool-surfaces](docs/reference/protocol-extensions.md#tool-surfaces) for the command surface |
| **See a bug class collapse to the same bytes across languages** | [docs/explanation/bug-zoo.md](docs/explanation/bug-zoo.md); run `cargo run --manifest-path bug-zoo/Cargo.toml -- --all` |
| **See a bug class map to an addressable shape CID across languages** | [docs/explanation/bug-zoo.md](docs/explanation/bug-zoo.md); run `cargo run --manifest-path bug-zoo/Cargo.toml -- --all` |
| **See supported languages and kit coverage** | [docs/reference/per-language-status.md](docs/reference/per-language-status.md) |
| **Understand the move** | [docs/papers/](docs/papers/) — recommended order: paper 03 → 06 → 02 |
| **Extend it / build a kit** | [docs/contributing/](docs/contributing/) |
Expand All @@ -111,7 +111,7 @@ For more entry points (per-language tutorials, IDE integration, publishing a `.p
- **Conforming implementations**: Rust, TypeScript, Python, Java, C#, Ruby, Zig, Go, C++, Swift, C, PHP. Coverage varies; see [docs/reference/per-language-status.md](docs/reference/per-language-status.md).
- **Protocol evolution**: PEP dogfoods catalog transitions as signed, content-addressed body-claims under `protocol/evolution/v1.6.1/` and `protocol/evolution/v1.6.2/`.
- **Content-addressed CI**: CICP binds CI results to exact source, protocol catalog, kit/toolchain, config, and accepted witness inputs. Reuse is allowed only when that closure is byte-identical.
- **Bug Zoo**: the self-contained `bug-zoo/` runner checks lab, exhibit, fixed, and wild specimen states; fixed pairs are accepted only after the same surface re-lifts to a clean boundary receipt.
- **Bug Zoo**: the self-contained `bug-zoo/` runner checks lab, exhibit, fixed, and wild specimen states; fixed pairs are accepted only after the same surface re-lifts or re-links to a clean boundary receipt.
- **Conformance gate**: catalog CIDs, proof-protocol fixtures, CICP vectors, self-contract attestations, and per-kit tests must agree before CI is green.

The protocol is content-addressed end to end. Each version's canonical name is its own catalog hash. Anyone with the spec bytes can verify that label locally. No central party decides what a version means; the bytes do.
Expand All @@ -120,21 +120,22 @@ The protocol is content-addressed end to end. Each version's canonical name is i

Bug Zoo is the executable lab for the claim above. Each specimen runs in an
isolated host-language environment, uses that language's own compiler/kit to
map source to a witnessed bug output, then checks that the canonical ProofIR
signature is byte-identical across surfaces and languages. The normal proof
gate for projects is `provekit prove`; Bug Zoo owns the fixture orchestration
under `bug-zoo/` and routes lift/proof work through the Rust CLI.
map source to canonical truth, then checks that the expected shape CID or
boundary receipt CID is addressable from that projection. The normal proof gate
for projects is `provekit prove`; Bug Zoo owns the fixture orchestration under
`bug-zoo/` and routes lift, link, and proof work through the Rust CLI.

The zoo is organized by species, not by language. A species directory owns a
`specimen.yaml` manifest, then each language under that species carries the same
lifecycle:

- `lab/`: ordinary host code that passes native checks while the bug class is
still latent. It has no ProvekIt workflow.
- `exhibit/<surface>/`: a native contract surface that lifts to the missing
edge and yields the red `provekit prove` signal.
- `fixed/<surface>/`: the paired source with that boundary closed, re-lifted
through the same surface to yield the green `provekit prove` signal.
- `exhibit/<surface>/`: a native contract surface that lifts or links to the
missing edge and yields the red `provekit prove` or `provekit link` signal.
- `fixed/<surface>/`: the paired source with that boundary closed, re-run
through the same surface to yield the green `provekit prove` or
`provekit link` signal.
- `wild/`: optional real upstream sightings pinned by advisory, commit, path,
and evidence.

Expand All @@ -145,12 +146,15 @@ k_lang(I) = t
```

`k_lang` is the language compiler as a ProvekIt kit/lifter, `I` is the source,
and `t` is the witnessed output: canonical ProofIR bytes, CID, and receipt.
and `t` is the canonical truth object: a ProofIR shape CID for claim
boundaries, or a LinkBundle receipt CID for cross-kit bridge derivations.
Different languages can disagree in syntax, runtime behavior, and exception
type while still compiling to the same witnessed `t`.
type while their native evidence maps homomorphically to the same addressable
shape.

Native evidence is projected into canonical truth; then the correctness layer
proves the missing edge or its closure.
Each native surface maps through a structure-preserving homomorphism into the
correctness object; the proof layer checks whether the mapped obligation
commutes with equivalent surfaces or closes under the fixed witness.

The current null-boundary receipts show Java, TypeScript, and C# lifting the same
missing edge:
Expand All @@ -169,13 +173,18 @@ They also run the red/green proof obligations through the Rust CLI: lab null is
rejected against each lifted non-null requirement, and each fixed surface
discharges the paired non-null implication with `provekit prove --formula`.

Read [docs/explanation/bug-zoo.md](docs/explanation/bug-zoo.md), or run:

Bug Zoo also carries value-scope escape as `BZ-SHAPE-006`: Java JUnit and Spring
exhibits both witness a point value, and the runner invokes
`provekit prove --formula` to produce the red signal when 42 fails a `>= 43`
requirement and the green signal when the fixed surface witnesses 43.

`BZ-SHAPE-007` carries the polyglot link-obligation specimen: a Go cgo caller
invokes a Rust callee whose native contract requires a stricter input. The zoo
routes the fixture through `provekit link`; the exhibit produces an
`unprovable-obligation` link-bundle receipt, and the fixed pair links clean.

Read [docs/explanation/bug-zoo.md](docs/explanation/bug-zoo.md), or run:

```sh
cargo run --manifest-path bug-zoo/Cargo.toml -- --all
```
Expand Down
1 change: 1 addition & 0 deletions bug-zoo/.gitignore
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
**/bin/
**/obj/
**/.classes/
Loading
Loading