Pith Number

pith:M63EQNBF

pith:2026:M63EQNBFTKJSQ7XCLNS6ZCDYTH

not attested not anchored not stored refs resolved

Caesar: A Deductive Verifier for Probabilistic Programs

Benjamin Lucien Kaminski, Christoph Matheja, Darion Haase, Joost-Pieter Katoen, Kevin Batz, Philipp Schr\"oer, Umut Yi\u{g}it Dural

Caesar translates HeyVL programs for probabilistic programs into verification conditions checked by Z3.

arxiv:2605.15827 v1 · 2026-05-15 · cs.PL

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

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{M63EQNBFTKJSQ7XCLNS6ZCDYTH}

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

Caesar translates HeyVL programs into verification conditions checked by Z3, with an additional probabilistic model-checking backend for a subset of HeyVL, after five years of development including new proof rules and better diagnostics.

C2weakest assumption

The underlying HeyLo logic and the added proof rules are sound, and Z3 is capable of deciding the generated verification conditions for the intended class of probabilistic programs.

C3one line summary

Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.

References

74 extracted · 74 resolved · 0 Pith anchors

[1] In: Silva, A., Leino, K.R.M 2021 · doi:10.1007/978-3-030-81688-9_1

[2] Affeldt, R., Cohen, C., Saito, A.: Semantics of Probabilistic Programs Using s- Finite Kernels in Dependent Type Theory. ACM Trans. Probab. Mach. Learn. 1(3) (2025).https://doi.org/10.1145/3732291 2025 · doi:10.1145/3732291

[3] Agrawal, S., Chatterjee, K., Novotn´ y, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Pro- gram. Lang.2(POPL), 34:1–34:32 (2018) 2018 · doi:10.1145/3158122

[4] Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL), 1–28 (2021).https://doi.org/10.11 2021 · doi:10.1145/3434333

[5] (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice 2016

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-20T00:01:20.581971Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

67b64834259a93287ee25b65ec887899d2c9b3a2ee33071ec35f8844984bc45f

Aliases

arxiv: 2605.15827 · arxiv_version: 2605.15827v1 · doi: 10.48550/arxiv.2605.15827 · pith_short_12: M63EQNBFTKJS · pith_short_16: M63EQNBFTKJSQ7XC · pith_short_8: M63EQNBF

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/M63EQNBFTKJSQ7XCLNS6ZCDYTH \
  | 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: 67b64834259a93287ee25b65ec887899d2c9b3a2ee33071ec35f8844984bc45f

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "433fb8ce3c7d907b51b96efcefbbf28f12ad6e60db688da3852106b271f745a0",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.PL",
    "submitted_at": "2026-05-15T10:27:07Z",
    "title_canon_sha256": "77c73cef480400495a3df8888416c0e5207ca44edf2b7daf2ef0ce3341227ba9"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15827",
    "kind": "arxiv",
    "version": 1
  }
}