Silica

Problem

Differential testing can show that instruction decoders disagree, but disagreement alone does not say which decoder is correct. I chose AArch64 because its fixed 32-bit instruction width makes a stronger experiment possible. There are exactly 4,294,967,296 instruction words, so validity can be checked across the complete space rather than estimated from a sample.

Silica began with a narrow question: where do Capstone, LLVM, and Unicorn differ from the architecture? Arm’s machine-readable XML specification supplied an independent reference. That choice turned the project from a comparison between implementations into a test against the architecture they were intended to model.

Approach

Verification was designed before the sweep engine. In February 2026, the repository added a seven-goal ledger and verifier stubs before most of the corresponding implementations existed. The project then grew in layers: a compiler for Arm’s XML diagrams, a compact specification oracle, in-process decoder adapters, normalization rules, bitmap storage, the sharded sweep, disagreement extraction, minimal reproducers, and reproducibility checks.

The full validity pass is exhaustive. Instruction text is not. Text comparison is much more expensive, so Silica clearly separates a deterministic one-million-word text sample from the complete validity results. This prevents the sampled result from being presented as a full-space claim.

Architecture

Rust owns the high-volume path. It calls the decoders in process and records one validity bit per instruction word for each oracle. The 32-bit space is divided into 256 shards, which can be run and verified independently. XOR over the resulting bitmaps exposes disagreement regions directly.

Python compiles the specification, normalizes decoder text, classifies findings, builds reports, and runs the independent verification layer. Crashing decoder calls are isolated and bisected until the exact instruction word is found. A separate silica-scope terminal reader opens completed artifact directories without loading the native decoder stack.

Validation

The exhaustive design exposed practical failures that a smaller run could miss. Concurrent shards first shared scratch directories and corrupted one another’s files. The fix gave every shard private scratch space. Unicorn could hang on some inputs, so the runner gained both process-level and emulator timeouts. The first disagreement verifier tried to materialize 724 million records, then had to be rewritten as a streaming check with a bounded per-shard cache.

The seven verifiers recompute coverage, disagreement integrity, normalization, metrics, reproducers, and the final result hash from artifacts. Each has a defect fixture that proves the check can fail. Pinned decoder versions make later runs comparable. The repository also records two limitations rather than removing them from the totals: Unicorn observes execution traps rather than decode validity, and some specification regions contain decode-time UNDEFINED conditions outside the compiled oracle’s current evaluation.

Results

Using Arm’s 2026-06 A-profile XML release, Silica checked all 2³² words. The specification allocated 1,799,435,776 encodings and left 2,495,531,520 unallocated. The run found 723,801,678 validity disagreements and reduced representative classes to ten filing-ready reproducers.

Agreement with the specification was 84.8 percent for Capstone, 87.6 percent for LLVM, and 88.3 percent for Unicorn. Those figures are not estimates. More important, they remain attached to the oracle definitions, scope exclusions, shard evidence, and known limitations that give the numbers meaning. Silica produced a large sweep whose result can be recomputed and disputed from the raw artifacts.