My First Paper: RuSMT

Back in July I wrote about filling the gaps in the Z3 Rust API. I mentioned a transpiler from Rust to SMT and that project is now my first published paper:

RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer
Mehrad Haghshenas and Meng Xu
SpecOps ‘26, the Workshop on Specification-Driven Development Life Cycle, Oakland, CA

The problem

Say you have a standard written in plain English, like the TOML spec, and a parser that claims to follow it. How do you check that it does? This is called conformance testing.

One known approach is to write the spec as a program. Then you run the program and the parser on the same input. If they disagree, one of them has a bug.

But this only checks the inputs you feed it. The inputs that matter most are often the error cases: that is where software tend to disagree with each other, and where code is least tested. Random or coverage-guided input generators can’t easily aim at one specific error.

What RuSMT does

You write the spec in a small subset of Rust. Each type stands for a Z3 sort, and each operation stands for a Z3 operation. Wherever the spec says “this is an error”, you put a named marker. Here is one from IMP, a tiny textbook language:

if *new_r.eq(I64::from(0)) {
    ArithmeticResult::Err(Path::named(String::from("division_by_zero")))
} else {
    ArithmeticResult::Ok(new_l.bv_div(new_r))
}

The same program is then used in two ways:

1. Compiled with rustc, it is the oracle. Give it an input and it tells you the correct result.
2. Translated to SMT-LIB, it gives one question per marker: is there an input that reaches this marker? Z3 tries to answer. If it finds an input, that input becomes a test.

When Z3 gets stuck, a language model guesses an input. Z3 then checks the guess. If the guess is wrong, Z3’s answer goes back to the model and it tries again. So the model proposes, Z3 decides, and the oracle confirms.

What came out of it

I wrote a TOML 1.1.0 parser in the DSL, about 5,900 lines, with 183 error markers.

• Z3 alone produced a test for 0 of the 183. Turning a whole recursive parser into one formula makes the formula too big to solve.
• With the language model in the loop, 146 of the 183 markers got a test.

I ran those 146 tests on four real TOML parsers: Rust’s toml, Python’s tomllib, Go’s BurntSushi/toml, and smol-toml for Node. On 12 inputs they didn’t all agree:

• 9 are cases the standard leaves open, like how big an integer can be.
• 2 are bugs in the Go parser that its maintainers already know about.
• 1 is a new bug. smol-toml accepts [[a], but that header needs two closing brackets. I reported it and added the missing cases to the shared toml-test suite.

Here is the whole thing on one page:

Links

• Paper (open access): doi.org/10.1145/3842652.3843196
• Code, data, and the recorded run: doi.org/10.5281/zenodo.22095547
• Google Scholar: citation page

Thanks to Meng for supervising the project and for presenting it in Oakland. If you have questions or feedback, feel free to reach out by email or GitHub.