Pith Number

pith:JERJI66U

pith:2026:JERJI66UV3U5FASD2ILRIYBD7C

not attested not anchored not stored refs resolved

Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair

Hongshu Wang, Jin Song Dong, Qin Li, Xinyue Zuo, Yamine Ait Ameur, Yuhan Sun

An LLM agent builds correct Event-B models from natural language by iteratively refining and repairing them with verification feedback.

arxiv:2605.17475 v1 · 2026-05-17 · 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{JERJI66UV3U5FASD2ILRIYBD7C}

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

Evaluation across systems of varying complexity demonstrates that Event-B Agent substantially outperforms baselines in end-to-end formal model synthesis and repair, while maintaining reasonable efficiency.

C2weakest assumption

The LLM can reliably translate formal verification error messages into sound repairs and refinements that preserve model correctness without introducing new inconsistencies or requiring human correction at each step.

C3one line summary

Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.

References

49 extracted · 49 resolved · 3 Pith anchors

[1] Jean-Raymond Abrial. 1996. The B-book: Assigning Programs to Meaning.Cambridge University Press(1996). doi:10.1017/CBO9780511624162 1996 · doi:10.1017/cbo9780511624162

[2] 2010.Modeling in Event-B: system and software engineering 2010 · doi:10.1017/cbo9781139195881

[3] GPT-4 Technical Report 2023 · doi:10.48550/arxiv.2303.08774

[4] Eman Alkhammash, Michael Butler, Asieh Salehi Fathabadi, and Corina Cîrstea. 2015. Building traceable Event-B models from requirements.Science of Computer Programming111 (2015), 318–338. doi:10.1016/j 2015 · doi:10.1016/j.scico.2015.06.002

[5] Anysphere, Inc. 2025. Cursor: The AI Code Editor. https://cursor.com/ Accessed: 2025-09-11 2025

Formal links

2 machine-checked theorem links

Receipt and verification

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

Canonical hash

4922947bd4aee9d28243d217146023f88149d4b34831b4ed8cc5c0adcfe1ca03

Aliases

arxiv: 2605.17475 · arxiv_version: 2605.17475v1 · doi: 10.48550/arxiv.2605.17475 · pith_short_12: JERJI66UV3U5 · pith_short_16: JERJI66UV3U5FASD · pith_short_8: JERJI66U

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/JERJI66UV3U5FASD2ILRIYBD7C \
  | 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: 4922947bd4aee9d28243d217146023f88149d4b34831b4ed8cc5c0adcfe1ca03

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "fad92d0e91eac4b0047d23c4d675e9ec7896be84af4e4abf205c79fc104db723",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.SE",
    "submitted_at": "2026-05-17T14:23:45Z",
    "title_canon_sha256": "2178f6178a735493e57eef348b75b3ed0a2977349db7f2fff83dd5e1a72c6d10"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.17475",
    "kind": "arxiv",
    "version": 1
  }
}