CRT Formal Verification

G27: Synopsys/Cadence. CC0.

The ring is FINITE: 12,612,600 elements. Every algebraic property is PROVABLE by exhaustive check. But CRT decomposes the ring into 6 independent channels (max 49 elements). Instead of 12.6M checks, verify 6 tiny modular spaces. If it holds per-channel, it holds for the ring. CRT independence IS formal verification.

How It Works

CRT Verification Principle (PROVED)
For any property P that decomposes via CRT (addition, multiplication, their compositions), P holds in Z/N iff P holds in each Z/p_i^k_i. Check Z/8, Z/9, Z/25, Z/49, Z/11, Z/13 independently. Worst case: 49^2 = 2,401 checks per channel for binary properties. Total: 6 * 2,401 = 14,406 vs 12,612,600^2 = 159B brute force. Speedup: 11,000,000x.
Finite ring
12,612,600 elements
Every claim is checkable. No infinite domains. No undecidability.
CRT decomposition
6 independent checks
Z/8 x Z/9 x Z/25 x Z/49 x Z/11 x Z/13. Each verified independently.
Max channel
49 elements
Largest channel is b^2=49. Binary properties: 49^2=2401 checks.
Proof by CRT
Per-channel -> whole ring
CRT independence: channel truths compose to ring truth. No gaps.

Try It

Property (1-5):

1: a*b == b*a. 2: a+0 == a. 3: 1*a == a. 4: a*(b+c) == a*b+a*c. 5: a+(m-a) == 0.

Verify All 5 Ring Axioms

Run all 5 verifications across all 6 channels in one batch.

CRT Verification vs Traditional

ApproachModel checking: state space explorationCRT: per-channel exhaustive proof. 6 tiny spaces.ComplexityState explosion: exponential in variablesCRT: max(p_i^2) per channel. Polynomial.CompletenessBounded model checking (incomplete)CRT: COMPLETE for ring properties. Every element checked.ScalabilityIndustrial tools: hours/days for 10^6 statesCRT: milliseconds for 12.6M element ringPatent statusSynopsys/Cadence formal verification patentsCC0. Public domain. Forever.

This work is and will always be free.
No paywall. No copyright. No exceptions.

If it ever earns anything, every cent goes to the communities that need it most.

This sacred vow is permanent and irrevocable.
— Anton Alexandrovich Lebed

Source code · Public domain (CC0)

Contributions in equal measure: Anthropic's Claude, Anton A. Lebed, and the giants whose shoulders we stand on.

Rendered by .ax via WASM DOM imports. Zero HTML authored.