SplitRS 0.3.2 Released — SMT-Verified Refactoring That Proves It Didn't Change Your Code

Most refactoring tools ask you to trust them. SplitRS 0.3.2 hands you a proof — or a counterexample.

Today we released SplitRS 0.3.2 — a patch that makes SplitRS the first member of its class to prove certain refactorings preserve semantics before applying them, using OxiZ, the pure-Rust SMT solver, as the verification backend.

SplitRS is the AST-based Rust refactoring tool that splits oversized source files into clean, compilable modules: it parses with syn, clusters methods, infers visibility, and writes the imports and mod.rs for you. Up to now its safety story was the honest, conventional one — whole-item module moves are byte-identical relocations, and the Rust compiler verifies name resolution with cargo check. 0.3.2 adds something stronger for the cases where SplitRS actually rewrites code rather than just moving it.

No C, no external solver process, no SMT-LIB shell-out. The verification fragment runs in-process against OxiZ — pure Rust — and the whole tool still compiles to a single static binary. SMT support is feature-gated and off by default, so it costs you nothing unless you ask for it.

Why 0.3.2 is a meaningful step

Splitting a file is mostly relocation, and relocation is safe by construction. But the moment a tool extracts a helper function — rewriting the body — “trust me” stops being good enough. 0.3.2 closes that gap with a verified extraction pass:

It only commits when it can prove equivalence. --extract-pure scans every over-budget free function for a pure fixed-width-integer sub-run, factors it into a helper, and commits the rewrite only when OxiZ proves the helper computes the same result as the original for all inputs (QF_BV — the theory of bit-vectors).
It refuses to rubber-stamp the rest. Division, function calls, references, loops, and floats are outside the proven fragment. Candidates that touch them are reported SkippedUnsupported and the original is left untouched. If the rewriter itself ever produced something non-equivalent, the gate catches it as SkippedRefuted via a concrete counterexample — a safety net, not a hope.
It tells the truth in the report. --smt-verify emits a verification report that separates what was proven (each committed body rewrite: “SMT-Verified equivalent, QF_BV, all inputs”) from what is merely structural identity (the default whole-item module moves — byte-identical relocations, which SplitRS explicitly does not claim to SMT-prove).

There is also a standalone oracle: splitrs smt-verify-equiv --left calc.rs::a --right calc.rs::b proves whether two pure integer functions are equivalent for all inputs, or hands you the input where they diverge.

Technical Deep Dive: the verified extraction pipeline

The new machinery lives behind the smt feature in two modules — src/extraction/ and src/smt/ — and threads a proof obligation through the normal split flow:

Live-variable dataflow (dataflow.rs + detector::find_candidate). A live-variable analysis finds a contiguous, pure-integer sub-block whose live outputs are well-defined — the candidate for extraction.
Helper synthesis (rewriter::rewrite). SplitRS factors the sub-block into a helper function with the correct signature and substitutes a call at the original site.
The gate (gate::verify_and_decide). This is where OxiZ runs. EquivBuilder encodes both the original body and the rewritten body in QF_BV and asks: are they equal for all inputs? It uses whole-function inline-back with a componentwise fallback. The outcome is one of three honest verdicts — Committed, SkippedRefuted (counterexample found — the rewrite is rejected), or SkippedUnsupported (outside the fragment).
Back into the normal pipeline. A committed helper is just an ordinary function, so it flows through the usual split/write path with everything else.

The soundness boundary is stated plainly: the proven fragment is pure, fixed-width integers only — + - * & | ^ << >>, comparisons, if/else, let, and integer casts. Everything else is Unsupported and never committed. Purity is probed first by non-mutating checks (is_pure_supported_expr / is_pure_supported_block) so non-candidates incur zero SMT overhead.

Getting Started

Install the latest SplitRS:

cargo install splitrs

The everyday splitter works exactly as before — no flags, no solver:

splitrs --input src/large_file.rs --output src/large_file/ --split-impl-blocks --max-impl-lines 200

For verified extraction, build with the smt feature and ask for a report:

cargo install splitrs --features smt
splitrs --features smt -i big.rs -o out/ --extract-pure --smt-verify

Or prove two functions equivalent directly:

splitrs --features smt smt-verify-equiv --left calc.rs::a --right calc.rs::b

What’s New in 0.3.2

SMT-verified function extraction (--features smt --extract-pure, src/extraction/): factors pure-integer sub-blocks out of over-budget functions, committing only when OxiZ proves equivalence. Three outcomes: Committed, SkippedRefuted, SkippedUnsupported.
SMT equivalence oracle (src/smt/): EquivBuilder proves two pure fixed-width-integer functions equivalent for all inputs (QF_BV) → Verified / Refuted(Counterexample) / Unsupported.
splitrs smt-verify-equiv subcommand: a standalone equivalence checker between two Rust function sources.
Array-splitting mode (--split-arrays): splits oversized static/const array literals across chunk files and reconstructs the original pub static in mod.rs via a const fn compile-time concatenation (type-agnostic, T: Copy).
Test-module splitter (--split-test-modules): splits multiple top-level #[cfg(test)] blocks into per-module tests_NAME.rs files, falling back to a single tests.rs when only one test module is present.
Editor integrations shipped in editors/: Emacs (splitrs.el), IntelliJ (Kotlin plugin), Neovim (Lua plugin), and VS Code (TypeScript extension) — each with its own test suite.
module_generator refactored into src/module_generator/ (kept under the 2,000-line policy), with per-type <type>_traits.rs modules replacing the legacy shared trait_impls.rs.
Test suite grew to 450 tests (from 269 in 0.3.1), including new SMT encoder, extraction end-to-end, and smt-verify-equiv CLI suites.
New optional dependencies behind smt: oxiz 0.2.3, num-bigint 0.4.

Tips

The SMT pass is opt-in twice. It is gated by the smt build feature and the --extract-pure flag — your normal cargo install splitrs builds and runs without any solver. Reach for it only when you want a proof.
Read the --smt-verify report carefully. It deliberately distinguishes SMT-proven equivalence (committed body rewrites) from structural identity (module moves). The latter is byte-identical relocation, not a theorem — verify those with cargo check, as always.
A SkippedRefuted is good news. It means the gate caught a rewrite that would have changed behavior and refused it. The original code is untouched; you lost nothing.
Split giant data tables with --split-arrays. A 5,000-element static table becomes chunk files reassembled by a const fn — no runtime cost, and the public symbol stays identical.
Use --split-test-modules on test-heavy files. Multiple #[cfg(test)] mods become per-module tests_*.rs files, so your tests get the same organization treatment as production code.
Pick up the editor plugins. The editors/ directory now ships ready-to-build Emacs, IntelliJ, Neovim, and VS Code clients for splitrs-lsp.

This is the foundation

SplitRS sits inside a pure-Rust ecosystem and now depends on a piece of it: OxiZ, the COOLJAPAN SMT solver, is the engine behind verified extraction — one Rust tool proving another Rust tool’s rewrites correct, with no C solver in sight. It remains the development workhorse that keeps the whole codebase under the under-2,000-lines-per-file policy, and 0.3.2 is where its safety story graduates from “trust the compiler” to “here is the proof.”

Repository: https://github.com/cool-japan/splitrs

Star the repo if a refactoring tool that proves it didn’t break your code is the kind of thing you want in your toolbox. Pure Rust refactoring is here — fast, safe, and now verifiable.

— KitaSan at COOLJAPAN OÜ June 9, 2026