ixyk: symbolic state diffs are all you need

· Support heartpunk on Patreon

Abstract

a proof of concept of the core of a symbolic-execution and anti-unification oriented technique [1] for extracting symbolic state transformers with guards and updates expressed as satisfiability modulo theories (smt) [3] using smt-lib [4] fragments interpreted with z3 [6]. the v0.0.2 release-tag campaign retained 765,233 hypothesis [9] differential-fuzz executions [8] comparing extracted models to unicorn [7] behavior across 98 of the 100 highest-frequency normalized x86-64 instruction families. tl;dr: it subtracts the old state from the new state, and that's the whole thing. just takes the definitions seriously.

Status

this is v0.0.2. it works. it is described in barely more than minimal form. additional versions will be coming w/clarifications and more explanation as i ascertain what exactly needs to go where. this is the first widely announced release. but it still does presume either specialized background or substantial interest.

also, literally just so i can move on to next steps.

Citation

v0.0.2 release has the version-specific DOI 10.5281/zenodo.22562518. the aggregate DOI is and resolves 10.5281/zenodo.22290191 to the latest release and all archived versions.

Sophie Smithburg. (2026). ixyk: symbolic state diffs are all you need (v0.0.2). Zenodo. https://doi.org/10.5281/zenodo.22562518

machine-readable citation metadata is available in CITATION.cff.

Getting Started

the pinned development environment is available through Nix. Docker provides the Linux/amd64 environment on macOS. run these commands from the repository checkout.

with Nix, the public ixyk development cache, hosted by Cachix, lets you download available prebuilt dependencies. no Cachix account or token is needed for downloads. enable it once, then enter the environment:

# one-time cache setup; runs Cachix without installing it permanently
nix run nixpkgs#cachix -- use ixyk
nix develop
ixyk-dev-check

the flake also declares the cache URL and signing key; accept those settings if Nix prompts for them.

with Docker, as an alternative:

export IXYK_UID="$(id -u)" IXYK_GID="$(id -g)"
docker compose pull dev
docker compose run --rm dev

then, inside the container:

ixyk-dev-check

Development

we use a p fuzzing and property based testing heavy approach here. in general, we try to exhaustively test the properties that matter wrt making sure the models we generate will be worth fuzzing, but overall, we rely on the differential fuzzing more than anything else. in some places we've measured coverage and done mutation testing, but not reliably. these are near term v0.0.3 targets. in the end, however, it will be more sensible to use our own models to prove our own correctness. that's probably at least in v0.x.0 territory, for values of x>=1.

most work has been done on osx and all build and test done on linux by way of linux based bazel clients triggering bazel REAPI actions.

Evidence outputs

the committed golden artifacts preserve the completed v0.0.2 release-tag REAPI run at a8a60a9, invocation 60862885-a2cf-4240-8fdc-0ce5a595e35f. they are observations from that revision. the corpus contains the 98 model and acquisition report pairs completed by that run; sar and imul are omitted for the scaling limitation described below.

• *.model.json.zst: losslessly compressed instruction models (ixyk.qf_abv.instruction.v1), or structured unavailable-model records.
• *.acquisition.json.zst: acquisition reports (ixyk.instruction_acquisition.v1), including status, model route, retained models, and findings. failed generalization can still leave usable direct models.
• *.fuzz.json: differential-fuzz reports (ixyk.differential_fuzz.v1), including actual execution counts, agreements, disagreements, incomplete processing, and any retained witness or replay checkpoint.
• *.evidence.zst: optional detailed event streams, distinct from the JSON summaries above.

the golden corpus has a SHA-256 manifest. existing fuzz summaries and run provenance accompany it; not every per-sample event stream is committed. ordinary compressed JSON can be inspected with zstd -dc FILE.json.zst.

catalog acquisition/fuzz actions are generated by catalog/validation_lanes.bzl from the probe catalog. detailed recording is off by default. the acquisition CLI and fuzz discover stage accept --recording reference-json, with --evidence-output, --commit, and --invocation-id. the caller supplies that provenance; the stream manifest records it.

event kinds are registered by evidence_types() in extractor/evidence_events.py. TypeRegistry reflects the dataclass field annotations; ReferenceJSONBackend.prepare() derives their encoding and decoding plans. the stream wraps JSON payloads in length-prefixed binary records, then applies zstd compression. it is not JSONL.

to read detailed streams, decompress them and use EvidenceReader with ReferenceJSONBackend() and evidence_types() from the recorded source revision. the reader exposes the manifest and typed records with IDs, timestamps, context links, and decoded values.

Validation

the abstract and tables below report the completed linux/remote execution api (reapi) [18] campaign from 2026-09-06, using the exact v0.0.2 source revision a8a60a9 and invocation 60862885-a2cf-4240-8fdc-0ce5a595e35f. the 10,000-example run completed in 34m38s wall time. it exercised the current constructor/source variation, nine-flag state model, and varied initial memory with recording enabled and shrinking disabled.

the campaign produced reports for 98 of the 100 highest-frequency normalized x86-64 instruction families. sar and imul were deliberately omitted after the preceding 100-example run exposed pathological expression-DAG traversal and tree-expanding serialization. those scaling bugs are tracked in #60 and #61; their omission is incomplete coverage, not a semantic result.

Profile	Reports	Requested per report	Full budget	Partial	Zero execution	Actual executions	Agreements	Disagreements	Unusable
100-example qualification	98	100	82	0	16	8,200	7,753	426	21
10,000-example campaign	98	10,000	71	11	16	765,233	723,041	40,694	1,498

10,000-example report status	Reports	Meaning
pass	44	every usable comparison agreed
mismatch	26	at least one concrete disagreement was retained
incomplete	28	the requested work could not all be completed; completed evidence was retained
total	98	980,000 examples requested

these statuses describe reports, not instruction correctness. a mismatch is a recorded model-versus-emulator difference for later classification; an incomplete report preserves the work established before a tool, generation, or resource boundary. failures do not erase independently acquired models or completed comparisons, and discovery continues through expected findings.

the committed corpus contains 98 compressed models, 98 compressed acquisition reports, and a SHA-256 manifest. detailed fuzz reports and event streams are not committed. complete replay support across every randomness boundary remains tracked in #62.

these measurements cover the current top-100 source catalog except for the two explicit omissions above. they do not claim coverage of every byte encoding or every dynamically executed x86-64 instruction. the existing validation-notes.md ledger preserves the earlier v0.0.1 campaign and its witness classifications as historical evidence.

Reference Artifacts

the deliberately versioned examples in artifacts/golden/ preserve exact acquisition, instruction-models. they are research reference artifacts, not ordinary bazel-bin/ or bazel-out/ contents. the directory documents what each example demonstrates, how to regenerate the set, and how to verify it against the pinned linux/reapi toolchain.

Repository Organization

• extractor/ — Python instruction-model pipeline.
  • artifact.py, typed_z3.py — canonical typed QF_ABV models and Z3 conversion.
  • extractor.py, amd64_state.py — Angr extraction and AMD64 architectural state.
  • model_syntax.py, operand_slots.py, instruction_schema.py — typed syntax exposure, decoded operand correspondence, and instruction-schema generalization.
  • fuzzer.py — differential validation against Unicorn.
  • CLI entry points, runtime adapters, and tests live alongside their implementation.
• antiunification/ — generic typed anti-unification algebra and its unit/property tests; currently housed here.
• Ixyk/ — Lean embedding.
  • QfAbv/ — typed syntax, expression semantics, and symbolic transition systems.
  • Artifact.lean — imports canonical model artifacts into the typed embedding.
  • GoldenCheck.lean, DifferentialEval.lean — artifact checking and executable differential evaluation.
• catalog/ — instruction selections, generated probes, and Bazel validation targets.
• artifacts/golden/ — checked-in compressed model artifacts and their checksum manifest.
• notes/ — research notes and exploratory censuses.
• tools/ — validation and CI tooling, including golden-artifact checks, Lean differential tests, and REAPI execution.
• third_party/ — vendored Python dependencies with Bazel integration.
• .github/ — CI workflows and shared actions.
• Root build files — Nix environments (flake.nix), Bazel dependencies/configuration, Python tooling (pyproject.toml), and Lean package/toolchain configuration.

Known Limitations

• intentionally linux only, bcz i didn't wanna focus on portability yet. should work on osx in principle p quickly. like. hard hard linux only. can only initiate build from linux client to linux server.
  • we have a docker container if u wanna work from osx! it could still be made portable in principle, but there just hasn't been a reason for it.
• this technique doesn't work really well for recursive opcodes. it could perhaps be generalized, but i just haven't tried yet.

Future Work

• for this repo
  • fill out the abstract, make easier understand for less specialized reader
  • doesn't yet work where the symex engine doesn't model enough. for example, VMENTER may be difficult to directly extract by symbolic state diffs.
    • the plan there is to read their defs out from emulators when they are defined in terms of instrs we already have, or to try other symex engines that do, or to cowardly admit defeat where we can't be perfectly total. still, i do expect in the end this can achieve higher coverage than prior instruction-semantics approaches [13]–[15]. TBD!
    • check the notes in the Intel x86 semantic-source union census.
  • turning the readme into a paper
  • floating point
  • extension to other ISA targets
  • further explanation of the proof story
• for those to come
  • STS stitching for full programs (prototyped)
  • futamura projection [17] of programs through implementations that have been assembled as a full STS (prototyped)
  • equivalence checking between hand generated or extracted STSes (prototyped)
  • lean proof of correctness of the technique (underway, quite confident should work out, but not certain yet)
  • eventually, fixed parameter tractable computation time detectors for many common weakness enumeration (CWE) [19] classes. this hasn't been done yet to any extent, but we have solid designs ready to prototype as time and priority permits.

References

1. J. C. King, “Symbolic execution and program testing,” Communications of the ACM, vol. 19, no. 7, pp. 385–394, 1976. doi: 10.1145/360248.360252.
2. T. A. Henzinger, R. Majumdar, and J.-F. Raskin, “A classification of symbolic transition systems,” ACM Transactions on Computational Logic, vol. 6, no. 1, pp. 1–32, 2005. doi: 10.1145/1042038.1042039.
3. C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Satisfiability, vol. 185, IOS Press, 2009, pp. 825–885. doi: 10.3233/978-1-58603-929-5-825.
4. C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard: Version 2.7. SMT-LIB Initiative, 2025.
5. Y. Shoshitaishvili et al., “SoK: (State of) the art of war: Offensive techniques in binary analysis,” in Proceedings of the IEEE Symposium on Security and Privacy, 2016, pp. 138–157. doi: 10.1109/SP.2016.17.
6. L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Proceedings of TACAS, LNCS 4963, 2008, pp. 337–340. doi: 10.1007/978-3-540-78800-3_24.
7. A. Q. Nguyen and H. V. Dang, “Unicorn: Next generation CPU emulator framework,” presented at Black Hat USA, 2015.
8. L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi, “Testing CPU emulators,” in Proceedings of ISSTA, 2009, pp. 261–272. doi: 10.1145/1572272.1572303.
9. D. R. MacIver, Z. Hatfield-Dodds, and contributors, “Hypothesis: A new approach to property-based testing,” Journal of Open Source Software, vol. 4, no. 43, art. 1891, 2019. doi: 10.21105/joss.01891.
10. Intel Corporation, Intel 64 and IA-32 Architectures Software Developer’s Manual, 2026.
11. G. D. Plotkin, “A note on inductive generalisation,” in Machine Intelligence 5, B. Meltzer and D. Michie, Eds. Edinburgh University Press, 1970, pp. 153–163.
12. D. M. Cerna and T. Kutsia, “Anti-unification and generalization: A survey,” in Proceedings of IJCAI, 2023, pp. 6563–6573. doi: 10.24963/ijcai.2023/736.
13. S. Heule, E. Schkufza, R. Sharma, and A. Aiken, “Stratified synthesis: Automatically learning the x86-64 instruction set,” in Proceedings of PLDI, 2016, pp. 237–250. doi: 10.1145/2908080.2908121.
14. S. Dasgupta, D. Park, T. Kasampalis, V. S. Adve, and G. Roşu, “A complete formal semantics of x86-64 user-level instruction set architecture,” in Proceedings of PLDI, 2019, pp. 1133–1148. doi: 10.1145/3314221.3314601.
15. J. Craaijo, F. Verbeek, and B. Ravindran, “libLISA: Instruction discovery and analysis on x86-64,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA2, art. 283, 2024. doi: 10.1145/3689723.
16. L. de Moura and S. Ullrich, “The Lean 4 theorem prover and programming language,” in Proceedings of CADE-28, LNCS 12699, 2021, pp. 625–635. doi: 10.1007/978-3-030-79876-5_37.
17. Y. Futamura, “Partial evaluation of computation process—An approach to a compiler-compiler,” Higher-Order and Symbolic Computation, vol. 12, no. 4, pp. 381–391, 1999. doi: 10.1023/A:1010095604496.
18. Bazel Project, “Remote Execution API,” bazelbuild/remote-apis.
19. MITRE, “Common Weakness Enumeration.”

License

Copyright (C) 2026 Sophie Smithburg.

Except where otherwise indicated, ixyk is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. See LICENSE for the full license text. Third-party components retain their own copyright and license terms.