[ANN] rpgm-decrypt — a formally-verified RPG Maker asset decryptor in OCaml

Ecosystem
1

Hi everyone))) :slightly_smiling_face:

I’d like to share rpgm-decrypt, a small command-line tool that decrypts and
extracts RPG Maker asset archives (XP / VX / VX Ace via .rgssad/.rgss2a/.rgss3a,
and MV / MZ via the XOR-encrypted assets and .pak archives).

It started as a clean-room reimplementation and ended up as an excuse to push
OCaml’s correctness tooling as far as I could on a real project:

  • Gospel specifications on the pure core ((*@ ... *) in the .mlis)
  • Why3 + Z3 deductive proofs of the key derivation, little-endian reads and a
    Zip-Slip path-safety invariant (23/23 goals discharged)
  • QCheck property tests (round-trip / invariants) alongside the unit suite
  • Coverage-guided afl-fuzz of the parsers in CI (0 crashes)
  • bisect_ppx coverage + a small directed mutation-testing pass
  • Ships as a single static binary via dune --profile static; the only external
    dep is camlzip (zlib) for the MZ .pak path

Build/test runs on the native Windows OCaml switch as well as Linux.
Licensed Apache-2.0.

Example run:

  $ rpgm-decrypt "MyGame" out
  scanned=1817 decrypted=1685 passthrough=132 skipped=0 failed=0 formats=[MV=1817]

Repo, docs and prebuilt Windows/Linux binaries:

Feedback on the spec/proof setup especially welcome — it’s my first serious go at
Gospel + Why3, so I’d love to hear how others structure that on real code.

6 Likes