Pressure-testing Ota on Grafana: bounded Go proof and a staged Compose slice

A case study on using the Ota tool (v1.6.25) to pressure-test a bounded, narrowly-scoped verification contract against the Grafana repository, covering only a Go package build path (./pkg/...) and a Compose slice of four observability dependencies (PostgreSQL, Prometheus, Loki, Tempo). The piece emphasizes explicitly what the contract does and does not prove, contrasting a narrow, honest claim against a misleading generic verify/build label, and links to a green CI matrix run as evidence.