Run the conformance suites

Badger is meant to work with any management backend that serves its contract: its own portal or the TestifySec platform. These suites let you check an implementation yourself instead of taking our word for it.

Portal HTTP contract

testifysec/portal/contract holds the suite and contract/cmd/portal-contract a runner. It checks:

• an anonymous request to sign a version gets 401 unauthenticated;
• an auditor's request to sign gets 403 forbidden;
• a request that names its own sequence gets 400;
• an administrator's request gets 201, and the next one gets the next sequence;
• an auditor's list shows the latest version;
• the trust document is well formed and its minimum sequence is the latest sequence;
• the history lists both versions, newest first, and an envelope comes back as the signed bytes;
• a deployment assignment succeeds, and re-pinning an older version is refused;
• the discovery document is served.

You need the CA that issued the portal's server certificate, and one client certificate with the admin role and one with the auditor role, issued for the test deployment only and kept in a private directory (certs below, mode 0700). From the repository root:

certs="$PWD/certs"
(cd testifysec/portal && go run ./contract/cmd/portal-contract -url https://portal-test.example.invalid:8443 \
  -ca "$certs/ca.pem" -admin "$certs/admin.pem,$certs/admin.key" \
  -auditor "$certs/auditor.pem,$certs/auditor.key")

It prints portal contract: pass and exits 0, or exits 1 and names the failure. It refuses a URL that is not HTTPS and never follows a redirect.

Formal model vectors

The onboarding model is on main; the contract model is in PR #182.

The Lean models export JSON vectors that the Go code replays. Each model has a check script that builds the model, refuses sorry, admit and native_decide, audits the axioms (only propext, Quot.sound and Classical.choice are allowed), and fails if the committed vectors are stale:

sh testifysec/formal/onboarding/check.sh
sh testifysec/formal/contract/check.sh   # PR #182, not on main yet

Each needs the Lean toolchain named in its lean-toolchain file (v4.34.1, core only, no Mathlib). The contract vectors cover 21 markings, 441 dominance and 441 join cases, 7 flows and 27 admission cases, which the Go connector and admission code replay. The onboarding vectors cover 27 traces of 168 steps; the Go replay test for them is not written yet.

Acceptance harnesses (available)

These compile the real executables and drive them against synthetic services on loopback. Each writes a JSON report that binds the source and executable hashes. Reports are unsigned local observations, not release evidence.

From the repository root:

# Admission: valid, tampered, wrong-key, expired, rollback, unknown-field and injection cases
(cd testifysec/managed && python3 uat.py --go "$(command -v go)" --bun "$(command -v bun)" --report /tmp/admission-uat.json)

# Gateway: streaming, credential isolation, denied-request audit, offline bounds, restart recovery
(cd testifysec/gateway && python3 uat.py --go "$(command -v go)" --report /tmp/gateway-uat.json)

# Portal: portal-signed profiles through the compiled hardened-admission
(cd testifysec/portal && python3 uat.py --go "$(command -v go)" --bun "$(command -v bun)" --report /tmp/portal-uat.json)

Run your platform against the contract

A backend conforms when it passes the portal HTTP contract and the workstation admits what it serves. The contract model in PR #182 states that a conforming backend's profiles are admitted whichever backend it is (conforming_backend_admitted); the backend vectors that would check this against running code have no Go consumer yet.