Experiment formal verification shards results 01 - kmosoti/FabricO11y GitHub Wiki
Hosted verification shard experiment, 18 October 2026
The preregistered two-runner pilot and canonical extended workflow both completed successfully for PR head c5f997e419280a62b2b7e81d8ec2460e737199af. Their actual checkout and receipt candidate was the same GitHub test merge commit faf148ec63e69826103b8fb0073aeaff4b0641e7. All ten extended check IDs, command vectors and property IDs match; all receipts report exit0, and their retained log hashes were independently rechecked. The final unchanged Python integrity/completeness validator ran successfully in both workflows.
- Canonical run
- Two-runner pilot
- Protocol committed before implementation
- Exact pilot workflow
- Bounded Rust collector
Observed critical path and cost
| Measurement | Canonical | Pilot |
|---|---|---|
| First job start to final job completion | 3061 s (51m01s) | 1776 s (29m36s) |
| Sum of runner job durations | 3061 s | 3377 s |
| Runners/jobs | One | Two check runners and one aggregate job |
In this single observed comparison the pilot reduced the measured job-to-completion critical path by 41.98%, while increasing summed runner time by 10.32% (316 s). Runner time is an elapsed-job proxy, not a billing-price calculation. The boundary excludes initial queue time before each workflow's first job starts. Both were triggered from the same PR update, but canonical started at 03:08:03 UTC and pilot at 03:06:36 UTC; this allocation difference is not credited as a scheduling benefit.
The semantic runner took 1603 s, the remaining-nine runner 1737 s, and aggregation 37 s. Actual post-containment setup markers measured 60.512 s and 72.490 s on the two check runners; check phases were 1506.635 s and 1639.339 s. Both restored a non-exact cache match. Canonical logs likewise report a restore-key cache hit with full match: false.
Pilot hardware was heterogeneous: semantic used four vCPUs on an AMD EPYC 7763 host, remaining used four vCPUs on an Intel Xeon Platinum 8573C host. Canonical CPU model was not explicitly recorded by its existing workflow. Thus hardware, setup/cache conditions and one non-randomized comparison limit attribution. This is evidence for a bounded two-runner scheduling trade-off, not a universal speedup estimate, CPU-normalized benchmark or GPU claim.
Complete check coverage
Individual receipt milliseconds below are attributed to each workflow and do not establish per-check speedup:
| Check | Canonical ms | Pilot ms |
|---|---|---|
| cargo-mutants | 600147 | 542203 |
| coverage-report | 385287 | 380427 |
| delivery-faults | 279419 | 283918 |
| dependency-policy | 1001 | 1017 |
| fuzz-smoke | 335480 | 338235 |
| kani-core | 73433 | 77154 |
| semantic-mutants | 1278371 | 1503354 |
| tla-delivery | 2477 | 2423 |
| tla-transport | 3655 | 3542 |
| trace-model | 5646 | 5440 |
The pilot assigns only semantic-mutants to one runner and the other nine original checks to the other. Each runner executes its assigned heavy checks serially through the unchanged contained launcher; max parallelism is two separate hosted runners. No local heavy concurrency was introduced. The collector requires exact disjoint artifact sets and performs bounded byte-preserving collection into DATA. It does not sanitize stale or corrupt bytes: the unchanged Python validator owns hash/source/completeness decisions. Failed or cancelled shards prevent aggregate success, while independent assigned checks retain their actual outcomes.
Preserved failure and correction
The initial pilot at a606ecc had two successful check shards but failed aggregate run 39090541570: artifact downloads were under the checkout rather than the DATA root, and the collector rejected them with DATA-only paths required. The final Python validator did not run in that failed aggregate. The failure, all shard bytes and raw log were retained. Correction c5f997e changed only experimental workflow paths and current-state prose to explicit $FABRIC_STORAGE_ROOT/results/verification-pilot/{shards,combined} locations. Collector guards and independent validator bytes were unchanged.
Original local focused checks at a606ecc and the correction's 23 CI contracts, 55 documentation probes and 10 hooks all exited 0 under containment. Current-head required fast/security/extended checks and the complete pilot succeeded before PR79 merged at 04:03:39 UTC, merge commit 0762513b1f44a5155973c332ad3b3c8ec397125d. The old superseded canonical run and redundant manually dispatched same-head run were cancelled and provide no required-gate credit.
This merge retains an experimental workflow; changing the canonical required workflow is a separate adoption/policy decision. A suitable adoption preserves the required extended context as the final aggregate verdict, all ten IDs and unchanged command/oracle semantics, exact disjoint collection, original Python validation, per-runner containment, actual failure propagation and complete artifact retention. No alpha acceptance or qualification was performed by these experiments; alpha remains owner-paused.
Audit records
DATA directory results/verification-shards-correction-01 contains full current canonical/pilot logs and downloaded artifacts, complete SHA256 inventories, per-job/per-step timings and hosted-paired-terminal-01.json. Earlier failed aggregate, cancellation observations and original source-focused receipts remain in their separate immutable paths. These actual source and run identities govern the comparison; no failed result was relabelled or reused as current success.
Canonical adoption and current-head evidence
PR80 integrated the native receipt verifier, bounded opt-in light-check scheduling and canonical two-host extended workflow in one review. It merged normally at 2026-10-18 05:11:53 UTC, main commit 06ccc0c4f3806028e923213e732ee4ed841a4c4a, after all five current-head checks succeeded: fast, security, both shards and the required extended aggregate. The original required check IDs, command vectors, proof bounds, independent Python product oracles and per-host containment remain. Heavy checks remain serial on each host; the original pilot is manual-only.
The consolidated PR head was 3c5c77375c9968c4352b49f0a030378f3c494da5. Its eight local integration commands completed with exit 0 and whole-cgroup stop at 04:38:56.166114 UTC, including 65 Rust tests, Clippy, formatting, 23 CI-contract tests and the documentation commands. Those local results belong to that source; wrapper SHA256 187e3629dd87eb654a6592dabcb2caf90c92dc3590462ddf0c5ad1923db9cec3.
The actual canonical extended run tested GitHub's synthetic merge c129013378d4bf65497d8af77a138102553b0686, independently observed in all three checkout logs and all archived receipts. This is distinct from both the PR head and final merge commit. Semantic completed at 05:05:27, remaining checks at 05:08:58 and the final aggregate at 05:09:46 UTC, all successful. The aggregate collected the exact ten original checks and ran the unchanged Python integrity/completeness validator. Its retained ZIP SHA256 is 96ffb40cc7858e8e5fc8d6a4416e8e8d289863654ed41f2ccfe3432da45275f4; DATA records under results/verification-adoption-integration-controls-01 retain the API metadata, full log, archive and hosted-current-terminal-01.json with ten shard receipts and their ten combined copies.
This establishes current-source integration and required CI completion, not a new speedup comparison. The earlier same-revision pilot/canonical pair above remains the measured comparison, with its hardware, setup/cache and total-runner-cost limitations. No GPU, product package rebuild, alpha qualification, release or tag is implied by verification-tool adoption.