SlimeJava — Measurement Procedure & Primary Data

This page consolidates the full verification data for Java → Rust bit-exact conversion — differential fuzzing, SMT formal proofs, Hybrid acceptance, performance benchmarks, exception boundaries, and seed injection. All of it uses deterministic seeds and is reproducible in a third party’s own environment.

For the product overview and positioning, see the product page. This page is the primary source for reproduction and verification.

1. Behavioral-invariance verification (differential testing)

Tests can show “there is a hole,” but cannot rigorously prove “there is no hole.” So we use the differential fuzzing (Csmith-style) proven in C-compiler validation: we byte-compare Java (the ground truth of two’s-complement wrapping) against the generated Rust. Because seeds are deterministic, any third party reproduces the same result, and any divergence reproduces the failing case verbatim.

Method	What	Cases	Result
Random differential fuzz (scalar)	2,250 random subset-Java programs (all operators, casts, ternary, bounded for, calls, corner literals)	53,932	✅ all byte-identical
Random differential fuzz (with arrays)	1,440 programs (adds array index read/write, length, new, OOB exceptions)	50,460	✅ all byte-identical
Exhaustive corner-case sweep	every binary op × extremal² {MIN,MIN+1,-1,0,1,2,MAX-1,MAX}, shift counts {-1..65}, int↔long promotion, casts, unary, ternary	2,900	✅ all byte-identical
Real OpenJDK Integer/Long verbatim	23 self-contained methods (bitCount/reverseBytes/nLZ/nTZ/compare/hashCode, etc.)	603	✅ all SHA-256 identical

~60,000 cases total, fully byte-identical to Java, zero divergence. Running 19,950 real methods through it produced zero false-accepts. The one mismatch surfaced was Java’s 64KB-per-method limit (harness-side, not a converter hole), resolved by splitting into sub-methods.

Differential testing shows the absence of holes within the test space with high confidence, but it is not a formal proof (that needs a verified validator / Coq). “No holes” here is meant in the practical sense. We avoid empty claims and never call an unmeasured region 100%.

2. Formal verification — SMT proof over all inputs

Differential testing is sampling. We model integers as two’s-complement = SMT bit-vector theory and have Z3 prove that, over all inputs, the converter’s output equals an independent mathematical specification (UNSAT = no counterexample = proven).

Target	Specification	Result
`bitCount` (32 & 64-bit)	== popcount (SWAR hex-mask chain equals population count)	✅ proven over all 2³² / all 2⁶⁴ inputs
`reverseBytes` / `rotateLeft/Right` / `signum` / `lowestOneBit`	byte-reverse permutation / rotate / sign / `i&-i`	✅ proven for both 32 & 64-bit (12 methods)
Division (b≠0): `a/b == bvsdiv` · `a%b == SRem` · remainder sign	round-toward-zero / sign follows dividend / sign property	✅ proven for both int/long
div-mod identity `a==(a/b)*b+(a%b)`	(nonlinear: division × multiplication)	⏱ timeout (undecided = needs bit-blast tuning, no counterexample)

Tally: 20 all-input formal proofs / 0 counterexamples / 2 timeouts. Zero counterexamples = no input violates bit-exactness. The only undecided item is the nonlinear div-mod identity (value & sign are already proven, so correctness is covered). Two-tier guarantee — primitives proven by SMT over all inputs; composition, loops, and arrays covered by ~60,000 differential cases.

3. Full Java = Hybrid Bit-Exact Isolate

“Full Java” does not mean rewriting everything into Rust; it means accepting all Java. Any Java is auto-partitioned into three regions, each given the strongest honest guarantee: static core → pure Rust (100% bit-exact) / dynamic → deterministic JVM Isolate (fixed-JVM 95-99%) / true nondeterminism → reject.

3-1. Acceptance rate (measured)

Corpus (real code)	Static→Rust	Dynamic→JVM Isolate	Nondeterm.→reject	Hybrid acceptance
Real OpenJDK Integer/Long/Math/Short	17.5%	82.1%	0.4% (native)	99.6%
Real app (19,950 methods)	0.5%	98.2%	1.3%	98.7%
Dynamic-heavy (reflection/lambda)	1.6%	98.4%	0%	100%

99% acceptance means “handles all Java,” but ≠ “all rewritten to Rust.” Only the static core (left column) rides the Rust fast path; the rest runs on the deterministic JVM Isolate. Rejects are true nondeterminism only (currentTimeMillis×84, getenv×50, nanoTime×22, Thread, Random, native). We never claim “always 100% across the whole Hybrid.”

3-2. Auto-partitioner + scale verification

Mixed Java in one command: classify → static core to a Rust dispatcher → dynamic to Isolate Java (static calls delegated to Rust across the boundary) → Hybrid run → byte-identity vs the original Java + certificate. We generated large volumes of random mixed Java to verify: 330 programs all byte-identical, 10,800 static cores Rustified, 2,259 boundary calls verified (zero divergence).

3-3. Exception-boundary marshaling

An exception thrown by the static core (Rust) is reproduced at the Java boundary as the same exception (type + message). Rust emits EXN\t<toString> → a Java stub dispatches on class name and re-throws the same type → toString matches exactly. /0 (ArithmeticException), array OOB (Index N out of bounds for length L), and new int[-n] (NegativeArraySize) were verified across the boundary in 1,053 crossings, all matching.

4. Performance — the value is “lightness & predictability”

Measured fairly on the same machine on ext4 (JVM warmup included, Rust in release). Throughput (hot steady state) is on par across all three. Rust wins on different axes:

Axis	JVM	GraalVM-native	Rust
Hot throughput (steady state)	roughly on par across the three (“Rust is faster” does not hold for hot integer work)
Startup (short-lived)	23.4 ms	1.25 ms	0.57 ms (~41×)
Peak RSS	41.2 MB	7.7 MB	1.9 MB (~22× smaller)
Deploy size	39 MB (minimal JRE)	8.8 MB	432 KB (~90× smaller)
Tail p99 (GC pressure)	9.92 ms (jitter 4.6×)	—	2.29 ms (jitter 1.1×)

The medians are on par (JVM 2.19ms / Rust 2.09ms), yet the JVM’s p99 jumps to 4.6× its median under GC pauses, while Rust stays flat with no GC (1.1×). Decisive for p99/SLA-bound workloads (trading, real-time, billing).

5. Seed-injection rescue (decisionism)

Nondeterminism rejects (unseeded Random, wall-clock) can be made deterministic by injecting a fixed seed / fixed clock and promoted into the static core. The honest crux: this *changes* behavior (a fixed seed ≠ free randomness), so bit-exactness is relative to the “fixed-seed version” = you *decide* how far to force determinism (decisionism, isomorphic to a PSDP safety-level profile). The original free randomness is not preserved.

Demonstrated: we inlined the LCG of java.util.Random.nextInt(), confirmed it matches new Random(seed) for all seeds, then Rustified that deterministic sequence to byte-diff 0. What cannot be rescued is I/O, true concurrency, and native (these stay rejected, honestly).

6. Implementation & reproduction

Everything is deterministic and re-runnable in a third party’s own environment (you can run the verification on their machine = a decisive difference from competitors).

bash run.sh                       # basic bit-exact
python3 fuzz.py 150 15            # random differential fuzz
python3 adversarial.py            # exhaustive corner-case sweep
python3 smt_validate.py          # SMT all-input formal proof (32/64-bit + division)
python3 slimejava_partition.py X.java   # Hybridize mixed Java in one command + certificate
python3 fuzz_hybrid.py 30 150     # Hybrid scale differential verification
sha256sum java.out rust.out      # third party diffs on their machine

7. Related links

SlimeJava product page SlimeNENC family SlimePython (modern) Request a PoC / contact