INV-003
Signing boundary scanner
scripts/check_signing_boundary.py
Static analysis pass that rejects any code path calling submit_and_wait without an explicit ward-signing-permitted marker. Runs on every CI push.
Last scanned: June 11, 2026
High-Assurance Infrastructure
Not a claim. A provable property.
Ward Protocol invariants are machine-checked, not just documented. TLA+ model checking, property-based tests in Rust and Python, and signing-boundary static analysis run on every CI push.
673 tests90% coverage on critical pathsTLA+ model checkedward_signed = False — always
Assurance snapshot
Core invariant
ward_signed = False — always
Formal verification
TLA+ SafetyInvariant, TLC checked in CI
Property tests
Hypothesis (Python) + proptest (Rust)
Static analysis
Signing boundary check on every push
The invariant
One provable property anchors everything.
Every formal artifact, every property test, and every static check traces back to this single structural guarantee. It is enforced in code, in CI, and in the TLA+ model simultaneously.
INV-001 — INV-003 · Signer boundary
ward_signed = False -- always.
Ward may: validate ledger state
construct unsigned transaction payloads
return deterministic conformance results
produce receipts
Ward must not: sign transactions
store private keys
request private keys
become custodian
become counterpartyEnforced by: signing boundary scanner (CI) · TLA+ SafetyInvariant (TLC) · proptest INV-003 (Rust) · Hypothesis INV-003 (Python)
Formal methods artifacts
Six machine-checked artifacts, all versioned in the repo.
These are not documentation. They are executable evidence. Each one runs in CI and fails the pipeline if the invariant is violated.
INV-003, INV-005, INV-018, INV-019, INV-023
Hypothesis property tests
tests/test_invariants_property.py
Property-based tests using Hypothesis. Arbitrary inputs generated across the full valid domain — no hand-written edge cases.
INV-003, INV-017, INV-018
Rust proptest invariants
ward/tests/invariants_test.rs
Proptest property tests against the Rust escrow crate. Verifies ward_signed=false, idempotency, and deterministic timing across all arbitrary inputs.
INV-007, INV-016
TLA+ formal specification
docs/formal/ward_validator.tla
TLA+ model of the nine-check conformance automaton and signing-boundary invariant. TLC model checker runs on every CI push.
INV-001 – INV-032
Protocol invariants register
INVARIANTS.md
32 hard invariants covering signer boundary, ledger authority, nine-check conformance, settlement, routing, and API surface. Human-readable source of truth.
All
High-assurance evidence log
HIGH_ASSURANCE.md
Maps each invariant to its machine-checked evidence: test file, property test, static checker, or model check. Audit trail for conformance reviewers.
Test coverage
673 tests. 90% coverage on critical paths.
Coverage is not the goal — correctness is. But coverage provides a lower bound on the evidence surface. These numbers are enforced in CI with per-module tracking.
Settlement
ward/settlement.py
Validator
ward/validator.py
Primitives
ward/primitives.py
Test suite breakdown
Unit tests
test_ward.py
Property tests (Python)
tests/test_invariants_property.py
Coverage gap tests
tests/test_coverage_gaps.py
SDK tests
sdk/python/tests/
Rust property tests
ward/tests/invariants_test.rs
TypeScript tests
sdk/typescript/
Nine-check conformance
Every check is an invariant, not a policy.
INV-007 states that a claim cannot pass unless all nine checks pass. There is no override, no emergency bypass, and no partial conformance. INV-016 closes the boundary — Ward returns unsigned instructions only.
INV-008
Policy artifact exists
Policy NFT located by ID and taxon (WARD_POLICY_TAXON = 281).
INV-009
Coverage window active
Policy expiry validated using XRPL ledger close_time — never server clock.
INV-010
Vault binding matches
Metadata vault address must equal the defaulted vault. Cross-vault claims fail.
INV-011
Default confirmed
LSF_LOAN_DEFAULT flag confirmed via authoritative LedgerEntry read.
INV-012
Loss is real and bounded
Vault loss must be greater than zero drops. Validated, not asserted.
INV-013
Coverage pool solvent
Pool usable balance must exceed loss amount. Reserve-adjusted.
INV-014
Policy still live
Policy NFT must not be burned, closed, or already settled. Replay protection.
INV-015
Claimant holds NFT
Claimant must still control the policy NFT at validation time, on ledger.
INV-016
Signer boundary holds
Even after all nine checks pass — Ward returns unsigned instructions only.
Audit readiness
Machine-checked evidence before the auditors arrive.
Ward Protocol targets Q3 2026 for a formal third-party audit. The formal artifacts, property tests, and static checkers described here form the pre-audit evidence package. They run continuously — not on request.
TLC model check in CI
TLA+ SafetyInvariant checked on every push via java -cp tla2tools.jar tlc2.TLC. Not a one-time artifact.
Signing boundary enforced at lint time
scripts/check_signing_boundary.py fails the pipeline if any code calls submit_and_wait without an explicit exemption marker.
Coverage enforced on critical paths
validator.py 89%, settlement.py 97%, primitives.py 87%. Tracked per module in CI with --cov-report=term-missing.
Formal specification versioned in repo
ward_validator.tla and INVARIANTS.md are versioned alongside the implementation. Specification drift is a CI failure.
Security Report · June 2026
Aikido Security rescan — 18 findings resolved.
An automated SAST/SCA scan was completed June 11, 2026. All critical and high-severity findings were remediated in-sprint. The full report is available for download.
673
Total tests passing
Python · Rust · TypeScript
18
SAST/SCA findings
All resolved or accepted
0
Open CVEs
As of June 11, 2026
Clean
Git history
Scrubbed June 11, 2026
Next steps
Review the specification. Discuss a pilot.
The assurance evidence is public and versioned. The full technical specification, conformance review, and integration surface are available without a sales call.