Formal Proofs & Audits

Relevant source files

The following files were used as context for generating this wiki page:

• launch-gates/PROOFGATE_EXECUTION_MANUAL.md
• launch-gates/COMPLETE_SYSTEM_SUMMARY.md
• launch-gates/INFRASTRUCTURE_STATUS.md
• launch-gates/SECURITY_AUDIT_ENGAGEMENT_GUIDE.md
• launch-gates/MAINNET_AUDIT_WORKFLOW.md
• scripts_infrastructure/install_x3_enforcement.sh
• vendor/zerocopy/agent_docs/reviewing.md
• knowledge-audit-report.md

The Formal Proofs & Audits system within the X3 project is an evidence-based framework designed to verify mainnet readiness. It replaces traditional percentage-based progress tracking with a rigorous "ProofGate" system, requiring every feature to be wired, tested, observable, recoverable, and reproducible before it is considered legitimate for production.

The system encompasses automated 12-step proof execution, invariant verification, AI-driven internal audits, and mandatory external security engagements. This multi-layered approach ensures that critical components—such as the Universal Asset Kernel, cross-VM bridge, and consensus logic—meet strict safety and determinism standards.

Sources: launch-gates/PROOFGATE_EXECUTION_MANUAL.md:4-7, launch-gates/INFRASTRUCTURE_STATUS.md:6-14

ProofGate Framework

ProofGate is the core infrastructure for generating and verifying evidence of system readiness. It utilizes a scoring system where features are assigned "Proof Tiers" based on the strength of the evidence provided.

Proof Tiers and Scoring

Features cannot score higher than their strongest attached proof. The system enforces a "No proof = no points" policy to prevent unsubstantiated claims of readiness.

Tier Level	Name	Description
10	code_exists	Feature exists only in documentation or comments.
25	code_created	Source code files are present in the repository.
35	wired	Feature is integrated into the runtime or API.
45	compiles	The code successfully passes cargo check.
55	unit_tested	Feature passes unit tests (cargo test).
70	integration_tested	Feature passes integration tests.
85	fuzz_invariant	Fuzz or chaos tests pass.
95	testnet_proven	Multi-node testnet proves the feature works at scale.
100	audit_approved	Formal proof or external audit approval.

Sources: launch-gates/PROOFGATE_EXECUTION_MANUAL.md:42-53, launch-gates/COMPLETE_SYSTEM_SUMMARY.md:65-76

12-Step Proof Execution

The automated verification process involves 12 specific steps to generate immutable evidence logs.

The 12-step sequence ensures everything from basic compilation to complex cross-chain logic is verified.
Sources: launch-gates/PROOFGATE_EXECUTION_MANUAL.md:58-132, launch-gates/INFRASTRUCTURE_STATUS.md:48-62

Critical Invariants

Invariants are system properties that must hold true at all times. ProofGate categorizes these into P0 (Release Blockers), P1 (High Priority), and P2 (Optional).

P0 Invariants (Hard Fail Gates)

If any of these invariants fail their respective tests, the system status is set to FAIL, and mainnet launch is blocked.

Invariant	Description	Required Proof
Canonical Supply	supply_in == supply_out; no phantom minting/burning.	x3-atlas-kernel supply tests
Atomic All-or-Nothing	Swaps must settle completely or roll back fully.	x3-atomic-trade rollback tests
Bridge Replay	Each message must have a unique nonce/hash.	x3-bridge replay tests
Timeout Recovery	Failed swaps must auto-rollback after 1 hour.	x3-atomic-trade timeout tests
No Prod Hazards	No panic!, unwrap(), or expect() in critical paths.	Regex Hazard Scan (rg)
State Consistency	Lock/unlock queues must match across VMs.	x3-bridge consistency tests
Runtime Weights	Every critical extrinsic must be benchmarked.	Weights file existence check

Sources: launch-gates/PROOFGATE_EXECUTION_MANUAL.md:136-157, launch-gates/COMPLETE_SYSTEM_SUMMARY.md:80-92

AI-Driven Audit Workflow

The project utilizes "Repomix" to package the codebase into AI-readable markdown files for automated auditing. These packs are processed using specialized prompts to identify architectural gaps.

Audit Lifecycle

The workflow follows a cycle of pack generation, AI analysis, and blocker remediation.

The workflow ensures that the AI auditor has specific context, such as bridge logic or runtime consensus, rather than the entire repository at once for better accuracy.
Sources: launch-gates/MAINNET_AUDIT_WORKFLOW.md:14-118, launch-gates/README.md:38-58

Specialized Audit Prompts

1. Wiring Audit: Verifies every module is connected to the runtime and identifies dead code.
2. Bridge Safety Audit: Focuses on replay attacks, finality reorgs, and cross-VM failure modes.
3. Invariant Hunter: Specifically searches for missing enforcement of P0 invariants.
4. Test Gap Audit: Identifies untested edge cases and missing failure path scenarios.

Sources: launch-gates/INFRASTRUCTURE_STATUS.md:85-110, launch-gates/COMPLETE_SYSTEM_SUMMARY.md:43-58

Mandatory Agent Rules & Enforcement

Automated agents (AI or scripts) must adhere to the AGENT_RULES.md to prevent "cheating" or weakening of the security posture.

Test Integrity and Consensus Safety

• No Weakening: Tests must not be modified to pass failing builds. Prohibited actions include removing assertions or skipping tests.
• Determinism: Consensus code must avoid non-deterministic sources (e.g., wall-clock time, unordered map iteration).
• Enforcement Script: scripts/x3_enforce.py scans diffs for assertion weakening (e.g., changing assert_eq! to assert!) and blocks commits if required artifacts like CONSENSUS_INVARIANTS.md are missing.

Sources: scripts_infrastructure/install_x3_enforcement.sh:37-140, vendor/zerocopy/agent_docs/reviewing.md:16-50

External Security Audits

External audits are mandatory for X3 mainnet launch to eliminate team bias and simulate real-world economic attacks.

Recommended Audit Firms

The project identifies tier-1 firms with specific expertise in Rust and Substrate:

• Trail of Bits: Focus on consensus, crypto, and formal methods.
• OpenZeppelin: Specialized in bridge code and EVM integrations.
• Zellic: Expert in Substrate runtime and cross-VM execution.

Sources: launch-gates/SECURITY_AUDIT_ENGAGEMENT_GUIDE.md:9-62

Audit Engagement Process

A standard engagement lasts approximately 17 weeks, from initial outreach to final re-audit verification.

Step	Phase	Key Action
1-3	Scoping	Define critical components (Asset Kernel, Bridge, Consensus).
5	Execution	Code freeze; auditors perform deep-dive analysis.
6-7	Remediation	Team fixes all Critical and High findings identified in the draft.
8-9	Finalization	Re-audit confirms fixes; final approval letter issued.

Sources: launch-gates/SECURITY_AUDIT_ENGAGEMENT_GUIDE.md:80-165

Summary

Formal Proofs and Audits in X3 are centered on the ProofGate system, which mandates a 100/100 readiness score before shipping. By combining automated invariant testing with multi-step AI audits and mandatory external reviews, the project ensures that its high-risk components—particularly the atomic cross-VM bridge—are secure against replay attacks and supply inconsistencies. Final mainnet readiness requires zero P0 blockers and a stable 72-hour testnet run.

Sources: launch-gates/README.md:96-105, FINAL_REPORT.md:36-47