Proposal: LLM-assisted skill for guided SMACK verification #837

Motivation

Using SMACK effectively requires more than invoking it with a fixed set of flags. A user must first determine whether the program and property are a good fit for bounded verification, choose models that match the source semantics, select justified loop and recursion bounds, and interpret counterexamples in light of SMACK's approximations.

An LLM-assisted SMACK skill could guide that process. The LLM would inspect the source and build configuration, form a verification plan, invoke SMACK with explicit precision and cost tradeoffs, and analyze any resulting error trace. The goal is not to present bounded verification as a proof of unrestricted correctness, but to make SMACK runs reproducible, appropriately configured, and easier to interpret.

PR #818 provides useful command-line and troubleshooting documentation that should serve as the skill's canonical reference rather than duplicating option documentation in prompts.

Proposed workflow

1. Source feasibility audit

Inspect the reachable source relevant to the requested property and report evidence with source locations:

• assertions, entry points, and selected properties;
• loops, recursion, inferred bounds, and nested-bound growth;
• signed overflow, unsigned/wrapped arithmetic, bitwise operations, shifts, narrow casts, and pointer/integer conversions;
• floating-point operations and floating-point/integer conversions;
• heap allocation, pointer manipulation, strings, concurrency, external calls, inline assembly, and unsupported constructs;
• build flags, macros, include paths, and whether assertions are actually declared.

The output should distinguish supported, conditionally supported, high-cost, and inconclusive features. Source inspection is only a hypothesis because preprocessing and compiler lowering can change what SMACK receives.

2. Translation probe

Before a full verification run:

• run translation with informational warnings enabled;
• retain LLVM and Boogie artifacts;
• confirm that assertions and requested property instrumentation survived compilation;
• inspect approximation and unsupported-operation warnings.

This step catches issues such as missing assertion declarations, absent sanitizer instrumentation in prebuilt bitcode, and semantics introduced during lowering.

3. Precision and cost plan

Choose the cheapest configuration that faithfully models operations relevant to the property, and change only one major precision dimension per diagnostic rerun. For example:

• use default unbounded integers for ordinary arithmetic;
• use wrapped integers when arithmetic wraparound matters but bit-level behavior does not;
• use bit-vectors for masks, shifts, bit-level casts, or other bit-dependent properties;
• enable precise floating point only when relevant, adding bit-vectors when floating-point/integer conversion requires them;
• disable memory splitting only as a targeted diagnostic;
• restrict entry points, checked functions, and properties where doing so preserves the verification goal;
• select loop, recursion, and concurrency bounds deliberately rather than increasing them blindly.

The skill must explain the semantic effect and expected scalability cost of every non-default option.

4. Reproducible execution

Record:

• the exact command and input/build recipe;
• SMACK, LLVM, verifier, and solver versions;
• selected properties, bounds, encodings, and memory model;
• result, runtime, warnings, trace, and generated artifacts.

Timeout and unknown results must remain inconclusive.

5. Counterexample triage

Reconstruct the source-level path and classify a trace as confirmed, likely real, likely modeling artifact, or inconclusive. A false-alarm conclusion must have supporting evidence, such as:

• the trace depends on an explicitly approximated operation and a rerun with the corresponding precise model eliminates it;
• concrete replay reproduces or refutes the reported behavior;
• a one-setting-at-a-time comparison localizes the result to a particular abstraction.

A timeout, solver disagreement, or disappearance under a more restrictive bound is not evidence of a false alarm. Failures reported inside SMACK's runtime model should be traced backward to the source operation that supplied the relevant pointer or value.

6. Qualified result

Reports should state exactly what was checked. For example:

No assertion violation was found through eight loop-header visits using unbounded integers, split memory regions, and the no-reuse-impls allocation model. Bitwise behavior remains approximate.

The skill must not reduce this to an unconditional "verified" result.

Important semantic guardrails

The initial implementation should encode the clarifications documented in #818:

• an explicit --check selection replaces the default assertion check rather than adding to it;
• --fail-on-loop-exit detects reachable normal loop exits, not paths truncated by unrolling, so it cannot establish bound adequacy;
• raw or prelinked bitcode must contain the instrumentation needed for checks such as signed integer overflow;
• successful and failing results are relative to the chosen bounds, models, and approximations.

Suggested MVP

Start with sequential C/C++ programs and support:

• assertions;
• integer-overflow checks;
• memory-safety checks;
• source and translation feasibility reports;
• a deterministic runner that stores a command manifest, logs, trace, and LLVM/Boogie artifacts;
• evidence-based trace classification.

Floating point and concurrency can follow after their precision and scalability policies are validated. The MVP should not explore a Cartesian product of flags or attempt to implement a new source parser; source and IR reasoning belongs in the LLM, while command execution and artifact capture should be deterministic.

Open design questions

• Should the skill live in this repository so its behavior evolves with SMACK's CLI and documentation, or in a separate skill repository?
• Which concrete examples should form its evaluation suite? Useful cases include loop-bound sensitivity, wrapped versus bit-vector arithmetic, floating-point approximation, a real memory-safety trace, and pointer/integer conversion interacting with memory splitting.
• What output schema would be useful both to humans and to future automation?