Pith Number

pith:SLGWLJ63

pith:2026:SLGWLJ63U6TKUYMNE222CB4OMW

not attested not anchored not stored refs resolved

Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution

Caleb Helbling, Graham Leach-Krouse, Michael Crystal

cozy performs comparative symbolic execution on original and translated binaries to flag differences for developer review while proving equivalence elsewhere.

arxiv:2605.12731 v1 · 2026-05-12 · cs.SE

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{SLGWLJ63U6TKUYMNE222CB4OMW}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

Outside of the flagged differences, the binaries are formally verified to be equivalent. Consequently, the review process guarantees equivalence modulo changes approved by the developer.

C2weakest assumption

That symbolic execution on the compiled binaries can exhaustively detect all semantic differences without missing behaviors or generating unmanageable numbers of spurious differences, and that the binaries faithfully represent the source-level semantics.

C3one line summary

cozy performs comparative symbolic execution on original and translated binaries to flag differences for developer review while proving equivalence elsewhere.

References

17 extracted · 17 resolved · 0 Pith anchors

[1] “Software memory safety,” National Security Agency, Tech. Rep., Apr. 2023. [Online]. Available: https : / / media . defense . gov / 2022 / Nov / 10 / 2003112742/ - 1/ - 1/0/CSI SOFTW ARE MEMORY SAFETY 2023

[2] Memory safe languages: Reducing vulnerabilities in modern software development, 2025

[3] The case for memory safe roadmaps: Why both c-suite executives and technical experts need to take memory safe coding seriously, 2023

[4] Back to building blocks: A path towards secure and measurable software, 2024

[5] Galois and Immunant,C2rust demonstration. [Online]. Available: https://c2rust.com/

Receipt and verification

First computed	2026-05-18T03:09:49.241418Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

92cd65a7dba7a6aa618d26b5a1078e6589e8f4bad84e3ec10b1542b041316d95

Aliases

arxiv: 2605.12731 · arxiv_version: 2605.12731v1 · doi: 10.48550/arxiv.2605.12731 · pith_short_12: SLGWLJ63U6TK · pith_short_16: SLGWLJ63U6TKUYMN · pith_short_8: SLGWLJ63

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/SLGWLJ63U6TKUYMNE222CB4OMW \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 92cd65a7dba7a6aa618d26b5a1078e6589e8f4bad84e3ec10b1542b041316d95

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "9936e0e510dabb980d7b497573463e426874924892f8a2b1c8f80b0d4632abe3",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by-nc-sa/4.0/",
    "primary_cat": "cs.SE",
    "submitted_at": "2026-05-12T20:33:33Z",
    "title_canon_sha256": "9ee5e7ffd9e082430dd659c124009109c67e7e34c2849fa34e9967f5b9f5a4eb"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.12731",
    "kind": "arxiv",
    "version": 1
  }
}