Machine-checked invariants
The policy boundary has executable contracts that describe the safety rules for every dispatch request. A symbolic checker can inspect the pure scalar logic.
Public evidence and scope
Laserreach Verified Core
Machine-checked policy boundaries for outbound eligibility and role-based access decisions, backed by reproducible production artifacts.
Verification passedReviewed September 3, 2026
What is checked
Two decisions. Explicit rules.
The outbound and access-control cores receive immutable values and return deterministic decisions. They have no database, network, clock, provider, or logging dependency. Existing integrations retain ownership of side effects.
- Missing or blank target identifiers are never eligible.
- Suppressed targets are never eligible.
- Unknown actions and non-positive requested counts are never eligible.
- A non-positive daily limit is never eligible.
- Usage plus the requested count must remain within the daily limit.
- Equal inputs produce equal decisions, and evaluation does not mutate inputs.
- Unknown roles never grant permissions.
- An explicit permission grant is honored without widening unrelated access.
- Wildcard access is granted only by a role or explicit wildcard permission.
Evidence layers
How the claim is tested
Deterministic examples
Representative allowed, malformed, suppressed, unknown-action, and over-budget requests lock the decision and reason shape used by the existing handler.
Property tests
Generated request values exercise the rules across edge cases such as empty identifiers, zero budgets, and counts at or above the configured limit.
Contract and browser tests
Integration contracts characterize policy and mailbox boundaries without provider I/O. Browser checks keep this page, its links, focus states, and scope copy discoverable.
Mutation testing
The verifier makes 198 controlled changes to the two policy cores. The tests reject every generated mutant, with no survivor or timeout.
Production artifact checks
Backend images use immutable base-image digests and exact dependency constraints. The build verifies installed versions and the bundled provider wheel before an image is accepted.
Reproduce the evidence
Source-bound results
Verified against backend revision ec07682b0941bf7ba5d5b3218d60ce59ed240e56 on September 3, 2026.
- Policy gate
- RUN_MUTATION=1 ./scripts/run_verified_checks.sh
- Regression gate
- pytest -q
- Policy results
- 55 focused tests · 100% of 74 statements and 38 branches · 198/198 mutants killed
- Model results
- CrossHair found no counterexample. TLC exhausted 1,389 distinct states with none left in the queue.
Toolchain: CrossHair, Hypothesis, mutmut, Coverage.py, Bandit, Ruff, and the TLA+ TLC model checker. Production Python resolution is constrained and checked during image builds.
Proof boundary
What this does not prove
The checks cover two pure policy functions, characterized integration boundaries, and production dependency resolution. They do not prove the complete Flask or Next.js application, Redis, DynamoDB, Unipile or other third-party providers and services, network delivery, scheduler behavior, account configuration, or deployed infrastructure.
Scope stays intentionally narrow
A passing check means the policy decision honored its stated inputs and the checked artifact matched its manifest. It does not mean an external action succeeded, a provider was available, or every surrounding workflow is covered. A separately tracked Next.js major-version migration remains outside this proof boundary.
Want the engineering context?
The public trust posture and press archive provide the surrounding context.