Skip to content

Claude support and doc updates - #520

Open
AdamZsofi wants to merge 19 commits into
masterfrom
claude-support
Open

Claude support and doc updates#520
AdamZsofi wants to merge 19 commits into
masterfrom
claude-support

Conversation

@AdamZsofi

@AdamZsofi AdamZsofi commented Jul 9, 2026

Copy link
Copy Markdown
Member

I started working on adding modular summaries per gradle package. As a side effect, I will also probably update some docs and have a list of possible smells/issues I/we can go through.

The root CLAUDE.md is unfortunately not optional, as that is the only place claude automatically adds it to context from - but I think that's fine.

The per package files are good, because they will only get loaded into context in a lazy manner, only when they are actually needed. But I will try to do most of core/common for sure.

I will probably not be able to generate these docs for all subprojects, so in the main CLAUDE.md I added an instruction for claude to ask the developer about also generating missing per-package docs when working with that given package. This also distributes reviewing these generated docs better over time and developers.

The generated docs are mainly about the code, rarely about an actual overview of methods or algorithms. However, they include "invariants", e.g., what to do to NOT break existing stuff and recipes, e.g., how to add a new formalism to cegar (some git history was checked for this), which I think is great. They might also be useful for developers, students, etc., not just agents.

How these docs were generated

The CLAUDE.md/USING.md files were produced by a phased, code-grounded workflow rather than written from memory:

  • Phase A (foundation): the module's core abstractions (~20 key files) are read in full, producing a "foundation digest" of contracts and conventions, plus a first draft reviewed by a human before proceeding.
  • Phase B/C (fan-out): the remaining packages are read exhaustively by parallel subagents — one per package group, each seeded with the foundation digest and a fixed extraction template (purpose / pattern deviations / key API / gotchas / cross-refs / suspected issues). No package summary is based on partial reads.
  • Phase D (reduce + verify): the digests are merged, and every concrete claim that enters a committed file is re-verified by grep/read against the source. Change recipes (e.g. "adding a new type touches X, Y, Z") are additionally grounded in the diffstats of real past commits (e.g. the EnumType addition) rather than inferred from structure.
  • Contradictions between code and existing docs, and anything bug-shaped, are not silently absorbed into the docs — they're collected in possible-issues.md for human triage.
  • File conventions: per-module CLAUDE.md = how to modify the module (invariants, recipes; auto-loaded when editing there); per-module USING.md = how to consume its API from elsewhere (loaded on demand); nested CLAUDE.md only where a subtree has its own repeated pattern (core/type). Conceptual overviews stay in READMEs.

@AdamZsofi

Copy link
Copy Markdown
Member Author

Current status

I consider the CLAUDE/USAGE.md files mostly done - maybe I will add the ones on the C frontend to this PR or maybe do that separately, but that is coming soon as well. But the core/common parts are done, in my opinion.

I also have a file called possible-issues.md, as the name suggests, it contains possible issues found in the meantime. I am not planning to leave that there, rather I want to go through it, and make issues and fixes for the relevant ones.

I am still working on improving the wiki and sorting out that part. But in the meantime, it would be nice to get some feedback on the generated files:

Files

Repo root

  • CLAUDE.md — extended: subproject map, documentation map, gradle naming, formatting,
    commit conventions, doc-upkeep rules, pointers to all USING.md files
  • possible-issues.md — ~50 bug-shaped findings from the code audits, grouped by module
    and severity; not yet reviewed — triage pending (includes one verified bug:
    smtlib's term parse-back maps bvmulBvAdd and swaps bvsrem/bvurem)

common/

  • common/CLAUDE.md + USING.md — utilities: deterministic-collection invariant,
    Logger levels, DispatchTable pattern, visualization, DSL scopes
  • core/CLAUDE.md + USING.md — Expr/Decl/Valuation vocabulary, the 5 core invariants
    (Decl identity!), expr-building & solver round-trip cookbook
  • core/…/type/CLAUDE.md (nested) — the type-family pattern + per-family deviations
    (bv signedness, fp rounding modes, non-evaluable exprs)
  • analysis/CLAUDE.md + USING.md — root interfaces, mutable-Proof CEGAR invariant,
    refinement pipeline; "bind your formalism" cookbook (CEGAR / MonolithicExpr / LTL
    paths, each verified against a real consumer)
  • analysis/…/algorithm/CLAUDE.md (nested) — checker landscape (CEGAR, BMC/k-ind/IMC,
    IC3, MDD, CHC, liveness), ARG covering/pruning mechanics, editing recipes
  • grammar/CLAUDE.md + USING.md — the parser for core's toString() format
    (machine round-trip, used by xcfa serialization) + Gson adapters

solver/

  • solver/CLAUDE.md + USING.md — the interface layer; getting/driving solvers
    (factories, managers, WithPushPop, unsat cores, interpolation, Horn, pooling),
    backend cheat-sheet with exact resolution strings ("Z3", "Z3:new", "JavaSMT:…",
    ":")
  • solver-z3-legacy/, solver-z3/, solver-javasmt/, solver-eldarica/ CLAUDE.md —
    per-backend notes: capabilities, version/naming gotchas, the transformer-mirroring
    obligation
  • solver-smtlib/CLAUDE.md — external-process machinery, installer framework,
    10-solver capability matrix with interpolation version gates, add-a-new-solver
    checklist

@mondokm , @as3810t may I ask you to take a quick look of the CLAUDE and USING files and the issue doc?

I don't need you to go through all of them, just read and leave a review on the ones that you think you know best. Feel free to recommend other reviewers for them, I just didn't want to ping too many people at once. :D
Thanks!

@mondokm

mondokm commented Jul 13, 2026

Copy link
Copy Markdown
Contributor

One thing that I noticed on first glance: the build info in the root CLAUDE.md is very xcfa specific, and .idea/workspace.xml (and the run config examples) does not exist in the repo, only on your machine.

Comment thread .github/workflows/linux-build-test-deploy.yml Fixed
Comment thread .github/workflows/linux-build-test-deploy.yml Fixed
@AdamZsofi
AdamZsofi requested a review from mondokm July 15, 2026 11:18
@AdamZsofi

Copy link
Copy Markdown
Member Author

/version-bump patch

@AdamZsofi

Copy link
Copy Markdown
Member Author

/version-bump patch

Comment thread .github/workflows/linux-build-test-deploy.yml Fixed

@mondokm mondokm left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we can merge this

Comment thread subprojects/common/analysis/README.md
@AdamZsofi

Copy link
Copy Markdown
Member Author

/version-bump patch

@AdamZsofi
AdamZsofi marked this pull request as ready for review August 17, 2026 11:36
@AdamZsofi
AdamZsofi enabled auto-merge August 17, 2026 11:48
@AdamZsofi

Copy link
Copy Markdown
Member Author

/format

@github-actions

Copy link
Copy Markdown
Contributor

Release Preview

Version: 7.3.2
Tag: v7.3.2

Release Notes:
Claude support and doc updates

I started working on adding modular summaries per gradle package. As a side effect, I will also probably update some docs and have a list of possible smells/issues I/we can go through.

The root CLAUDE.md is unfortunately not optional, as that is the only place claude automatically adds it to context from - but I think that's fine.

The per package files are good, because they will only get loaded into context in a lazy manner, only when they are actually needed. But I will try to do most of core/common for sure.

I will probably not be able to generate these docs for all subprojects, so in the main CLAUDE.md I added an instruction for claude to ask the developer about also generating missing per-package docs when working with that given package. This also distributes reviewing these generated docs better over time and developers.

The generated docs are mainly about the code, rarely about an actual overview of methods or algorithms. However, they include "invariants", e.g., what to do to NOT break existing stuff and recipes, e.g., how to add a new formalism to cegar (some git history was checked for this), which I think is great. They might also be useful for developers, students, etc., not just agents.

How these docs were generated

The CLAUDE.md/USING.md files were produced by a phased, code-grounded workflow rather than written from memory:

  • Phase A (foundation): the module's core abstractions (~20 key files) are read in full, producing a "foundation digest" of contracts and conventions, plus a first draft reviewed by a human before proceeding.
  • Phase B/C (fan-out): the remaining packages are read exhaustively by parallel subagents — one per package group, each seeded with the foundation digest and a fixed extraction template (purpose / pattern deviations / key API / gotchas / cross-refs / suspected issues). No package summary is based on partial reads.
  • Phase D (reduce + verify): the digests are merged, and every concrete claim that enters a committed file is re-verified by grep/read against the source. Change recipes (e.g. "adding a new type touches X, Y, Z") are additionally grounded in the diffstats of real past commits (e.g. the EnumType addition) rather than inferred from structure.
  • Contradictions between code and existing docs, and anything bug-shaped, are not silently absorbed into the docs — they're collected in possible-issues.md for human triage.
  • File conventions: per-module CLAUDE.md = how to modify the module (invariants, recipes; auto-loaded when editing there); per-module USING.md = how to consume its API from elsewhere (loaded on demand); nested CLAUDE.md only where a subtree has its own repeated pattern (core/type). Conceptual overviews stay in READMEs.

Modified subprojects (since v7.3.1):
common/analysis
common/common
common/core
common/grammar
common/ltl
frontends/c-frontend
frontends/chc-frontend
solver/solver
solver/solver-eldarica
solver/solver-javasmt
solver/solver-smtlib
solver/solver-z3
solver/solver-z3-legacy
xcfa/cat
xcfa/xcfa
xcfa/xcfa-cli
xsts/xsts
xta/xta

Files to be uploaded:

@AdamZsofi
AdamZsofi added this pull request to the merge queue Aug 17, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Aug 17, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Benchexec test report for a selection of benchmarks (correct / incorrect / all):

Rundefinition Correct Incorrect All Status
CHC-COMP_Portfolio 147 0 195
Hardware_CEGAR 47 0 54
PLC_CEGAR 9 0 9
PetriNet_MDD 60 0 122
PetriNet_PN_MDD 72 0 122
SV-COMP_Portfolio_Emergent 154 0 168
SV-COMP_Portfolio_Horn 120 0 168
SV-COMP_Portfolio_Stable 164 0 168
Statechart_CEGAR 110 0 126

📦 Download the results - extract the zip and open the *.html files.

@AdamZsofi
AdamZsofi added this pull request to the merge queue Aug 17, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Aug 17, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants