Governance Proofs

Governance proofs are project-wide properties checked against every relevant call site in your codebase. Unlike per-function annotations that verify one function at a time, governance proofs are universally quantified: every X in the codebase must satisfy Y. This is how you close the gap where a passing test suite coexists with a real hole, because a test only looks where you pointed it and a governance proof looks everywhere.

After this page you will be able to attach a governance property to a project, understand the categories the platform library covers, read and triage violations, set severity, suppress an intentional exception with a recorded reason, and map results to the compliance frameworks your auditors care about.

Governance proofs are part of Backbuild Prove, which is launching soon. Join the waitlist to get access at launch.

A single governance rule at the top reads: every request handler checks authorization before acting. Arrows fan out to three source files below. Inside each file, individual call sites are listed; most show a green check, and two sites, one in the orders file and one in the reports file, show a red cross and are flagged as violations. A caption reads: one rule, checked at every matching call site across the codebase, on every commit. — One governance rule is checked at every matching call site across the whole codebase, on every commit. Sites that do not satisfy it are flagged individually by file and line.

What Governance Proofs Are

A governance proof is a formally stated property that applies across your entire project. When attached to a project, Backbuild Prove identifies every relevant call site and verifies that each one satisfies the property. A single governance theorem can generate hundreds of verification checks across a large codebase.

Examples of governance proofs:

Every authenticated request validates the session before reading user data
Every multi-tenant data query is scoped to the calling tenant
Every password comparison uses a constant-time comparison function
Every PII field is encrypted before storage
Every state-changing request validates an anti-forgery token
Tenant data is isolated so one tenant’s records are never returned to another
Every write operation emits an audit log entry

How It Works

Backbuild Prove publishes governance theorems. The platform team maintains a library of formally stated governance properties covering security, compliance, and architectural patterns.
You attach theorems to your project. From the Governance screen in the Backbuild dashboard, select the theorems that apply to your project.
Verification runs on every backbuild prove run. The kernel reads each attached theorem, identifies matching call sites in your codebase, translates them to the kernel's term language using the language parser, and verifies each one against the governance property.
Violations are recorded. Any call site that fails verification is recorded and surfaced in the Governance Violations tab of the Prove dashboard.

Illustration of a governance violations dashboard. The top lists attached rules, each with a severity of error, warning, or ignored, and a count of matching call sites. Below is a violations list where each failing site shows its file and line, its category, and the compliance control it maps to. One row is expanded to show a suppression with a recorded reason. — Illustration: the governance dashboard lists each attached rule with its severity and coverage, and every failing site with its category, mapped control, and any recorded suppression. Backbuild Prove is launching soon.

What a Governance Proof Establishes

A governance proof establishes its stated property at each matching call site given the assumptions cited at trust boundaries. It is not pattern matching and it is not a promise that a whole category of vulnerability is impossible everywhere; it is a proof that, at each site the check applies to, the property holds under the stated assumptions. The curated theorem library defines precisely what each category checks and what it assumes, so the result is auditable rather than a black box. Where a call site uses a construct the parser cannot translate, the check reports parser_skip for that site rather than silently passing it, so coverage is visible.

Library Categories

Governance theorems are organized into categories. Each category covers a specific domain of security or compliance concern.

Category	Description
`auth`	Authentication and session validation
`rls`	Row- and record-level access control enforcement
`tenant_isolation`	Multi-tenant data separation
`crypto`	Cryptographic best practices
`sql_injection`	SQL injection prevention
`xss`	Cross-site scripting prevention
`csrf`	Cross-site request forgery prevention
`pii`	Personally identifiable information handling
`audit_logging`	Audit trail completeness
`rate_limiting`	Rate limit enforcement
`memory_safety`	Memory safety guarantees
`concurrency`	Thread safety and race condition prevention
`compliance`	Regulatory compliance requirements

Compliance Framework Coverage

Governance theorems map directly to specific controls in major compliance frameworks. When you attach a theorem, the dashboard shows which compliance controls it satisfies.

PCI DSS 4.0

Control	Description
3.5	Render stored cardholder data unreadable (PAN protection)
6.2.4	Software defenses against injection (SQL injection, XSS, CSRF)
7.2.1	Access control to system components for authorized individuals
8.3.1	Strong cryptography for authentication credentials
10.2.1	Audit logs for access to cardholder data

SOC 2

Control	Description
CC6.1	Logical access security over information assets
CC6.7	Restriction of data transmission and removal
CC7.2	Monitoring of system components for anomalies

ISO 27001:2022

Control	Description
A.8.3	Information access restriction
A.5.17	Authentication information
A.8.24	Use of cryptography
A.8.15	Logging

HIPAA

Control	Description
164.312(a)(1)	Access control
164.312(b)	Audit controls
164.312(e)(2)(ii)	Encryption of ePHI in transit

Additional Frameworks

Framework	Controls
GDPR	Article 32: Security of processing
OWASP	A01: Broken Access Control, A03: Injection
CWE	79 (XSS), 89 (SQL Injection), 352 (CSRF)

Severity Override

Each governance theorem attachment has a configurable severity level that determines how violations are treated:

Severity	Behavior
`error`	Violations fail the verification run. The `backbuild prove run` command exits with a non-zero status.
`warning`	Violations are reported but do not fail the run. Useful during gradual adoption.
`ignored`	The theorem is attached but not enforced. Violations are not checked or recorded.

Suppressing Individual Violations

Individual governance violations can be suppressed when a call site is intentionally exempt from the governance rule. Suppression requires a reason, which is recorded in the audit trail for compliance purposes.

Suppressions are visible in the Governance Violations tab and can be reviewed, approved, or revoked by project administrators. The suppression reason is included in compliance reports and formal proof printouts.

Custom Governance Theorems

In the initial release, governance theorems are curated and maintained by the Backbuild Prove platform team. This ensures that every theorem in the library is formally sound and correctly matches the intended code patterns.

Enterprise custom theorems are planned for a future release. Enterprise customers will be able to author custom governance theorems specific to their organization’s policies and architectural standards.

Limitations

Parser support required. The language parser must support the constructs used at each call site. If the parser cannot translate a construct, it is reported as parser_skip and the governance check does not apply to that call site.
Static analysis only. Governance proofs verify code statically at verification time. They do not monitor runtime behavior. Use runtime monitoring and observability tools alongside governance proofs for complete coverage.
Library grows over time. New governance theorems are added to the platform library regularly. The set of available theorems expands as the Backbuild Prove team formalizes additional security and compliance patterns.

Can I assert a property holds at every call site, not just where a test looked?
Yes. That is the whole point. A governance theorem is universally quantified, so Prove identifies every matching call site and checks each one. A single theorem can generate hundreds of checks, and a site that is missing the required control is flagged as a violation with its file and line.

How is a proof of "no injection here" actually grounded? What is assumed versus proved?
The proof establishes the category's stated property at each site given the assumptions cited at trust boundaries; it is not a pattern match and not compliance theater. The curated library defines exactly what each category checks and assumes, so a reviewer can see the basis of every result. See What a Governance Proof Establishes.

Can I author my own governance theorems for my threat model?
Not yet. At launch the library is curated and maintained by the platform team, so every theorem is formally sound and matches the intended patterns. Enterprise custom theorems are planned for a future release; they are not available today, and this page does not describe them as live.

Does this replace runtime monitoring?
No. Governance proofs verify code statically at verification time. Keep your runtime monitoring and observability for behavior that only exists at runtime; use governance proofs to prove the static property holds everywhere.

Next Steps

Writing pf2 Annotations: per-function proof annotations
Certifications: formal proof certificates for compliance audits
Pre/Post Contracts: precondition and postcondition verification
Project Settings: configuring governance attachments and severity