CRT Formal Verification

Synopsys/Cadence patents. CC0 alternative.

The ring is FINITE: 214,414,200 elements. Every algebraic property is PROVABLE by exhaustive check. But CRT decomposes the ring into 7 independent channels (max 49 elements). Instead of 214M checks, verify 7 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, Z/17 independently. Worst case: 49^2 = 2,401 checks per channel for binary properties. Total: 7 * 2,401 = 16,807 vs 214,414,200^2 brute force. Speedup: ~2.7 trillion x.
Finite ring
214,414,200 elements
Every claim is checkable. No infinite domains. No undecidability.
CRT decomposition
7 independent checks
Z/8 x Z/9 x Z/25 x Z/49 x Z/11 x Z/13 x Z/17. Each verified independently.
Max channel
49 elements
Largest channel is 7^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 7 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 214M element ringPatent statusSynopsys/Cadence formal verification patentsCC0. Public domain. Forever.

Source code · Public domain (CC0)

Report issue

.ax source compiled to WASM via self-hosting compiler. Zero HTML authored.