Metadata-Version: 2.3
Name: speclogician
Version: 1.3.0
Summary: SpecLogician is an AI framework that turns code, tests, logs, and requirements into mathematical context for LLMs through formal specification synthesis, verification, and analysis.
Author: denis, hongyu
Author-email: denis <denis@imandra.ai>, hongyu <hongyu@imandra.ai>
Requires-Dist: imandrax-api-models>=19.0.0
Requires-Dist: iml-query>=0.5.1
Requires-Dist: pydantic>=2.12.5
Requires-Dist: pyperclip>=1.9.0
Requires-Dist: rich>=14.2.0
Requires-Dist: textual>=6.11.0
Requires-Dist: textual-image>=0.6.0
Requires-Dist: textual-plotext>=1.0.0
Requires-Dist: tree-sitter>=0.25
Requires-Dist: tree-sitter-iml>=0.26
Requires-Dist: typer>=0.24
Requires-Python: >=3.12
Project-URL: Homepage, https://speclogician.dev/
Description-Content-Type: text/markdown

# SpecLogician

SpecLogician is an AI framework for building, maintaining, and analyzing the **mathematical context** of a software project.

www.speclogician.dev

## Installation

```bash
curl -fsSL https://speclogician.dev/install.sh | sh
```

The installer bootstraps [`uv`](https://github.com/astral-sh/uv) if needed, then installs SpecLogician into its own isolated Python 3.13 environment. No system Python required.

To pin a specific version: `SPECLOGICIAN_VERSION=1.1.3 curl -fsSL https://speclogician.dev/install.sh | sh`.

Verify with `speclogician --help`.

## Quick start

```bash
# Explore a bundled demo (10 available: see `speclogician demo ls`)
speclogician demo run bank-account
speclogician demo tui bank-account        # interactive terminal UI
speclogician demo shell bank-account      # Python REPL with state loaded

# Generate the canonical agent prompt for use with an LLM coding agent
speclogician prompt --out PROMPT.md

# Initialize and build your own spec
speclogician ch base-edit --src "type state = { x : int }\ntype action = { y : int }"
speclogician ch pred-add  --pred-type state --pred-name x_positive --pred-src "s.x > 0"
speclogician ch trans-add --trans-name step --trans-src "{ x = s.x + a.y }"
speclogician ch scenario-add grow --given x_positive --then step --initial \
  --description "From a positive position, applying the action grows it further."

# Inspect the current state
speclogician view state --compact
speclogician reach summary
```

State is persisted to `sl_state.json` in the current directory.

### Dashboard

A web-based dashboard renders the spec, reachability graph, complement regions, and artifact links interactively:

- **VS Code extension**: install the SpecLogician extension and click the **SpecLogician** or **Browser** button in the status bar.
- **Standalone**: install the `speclogician-dashboard` node binary (shipped with the VS Code extension's npm package), then `speclogician-dashboard ./sl_state.json` opens it in your default browser.

Both surfaces are driven by the same `sl_state.json` and update live as you apply changes.

## Learn more

- **Bundled demos** — `speclogician demo ls` lists them. Each demo is a complete formalization showing one specific pattern (bank account, traffic light, stock exchange order matching, …).
- **Tutorial walkthrough** — `tutorial-2/` contains a hand-built spec with slides, narrated step-by-step. The `tutorial/` folder is the manual-formalization companion (raw IML, no SpecLogician CLI).
- **Agent guide** — `speclogician prompt` outputs a thorough document explaining the modeling workflow, granularity discipline, and how to compose predicates / transitions / scenarios. Feed it to an LLM coding agent before delegating formalization tasks.
- **CLI reference** — every command supports `--help`. Top-level commands: `ch`, `view`, `find`, `reach`, `demo`, `undo`, `prompt`, `tui`.
- **Web docs** — [speclogician.dev/docs](https://speclogician.dev/docs).
- **Companion tool** — [CodeLogician](https://codelogician.dev) is the recommended IML authoring companion. The cross-tool workflow is *read code → translate with CodeLogician → formalize with SpecLogician*.

---

## 1) The challenge: software lacks mathematical context

Modern software projects accumulate many forms of partial understanding:

- source code
- tests
- execution traces
- bug reports
- requirements
- design documents
- operational knowledge held by engineers

But these artifacts do **not** usually form a precise, machine-checkable understanding of system behavior.

This becomes a serious problem for both humans and AI systems:

- code alone does not make intent explicit
- tests only sample behavior
- documentation is incomplete and drifts
- execution traces are local observations, not general models
- LLMs can manipulate software artifacts, but they do not automatically construct a rigorous behavioral understanding of the system

As a result, software projects often lack a durable mathematical representation of:

- what the system is allowed to do
- what it must never do
- how state evolves
- which scenarios are covered
- where ambiguity, inconsistency, or incompleteness remains

SpecLogician is built around the idea that software projects need this missing layer: **mathematical context**.

---

## 2) Core idea: build mathematical context incrementally

SpecLogician is an AI framework for constructing formal understanding of a software system from the artifacts that already exist around it.

Rather than requiring a large monolithic formal model upfront, SpecLogician builds mathematical context incrementally through structured, local, machine-checkable pieces.

Its core representation combines:

- **symbolic scenarios** written in a structured `given / when / then` style
- a **domain model** that captures the underlying state, actions, predicates, and transition structure
- links to concrete project artifacts such as:
  - source code
  - tests
  - logs
  - traces
  - documents

This allows a software project to evolve toward a formal behavioral model gradually, instead of requiring a single canonical specification to be written all at once.

The result is not just “a spec,” but a growing mathematical account of the project’s behavior.

---

## 3) What “mathematical context” means in practice

In SpecLogician, mathematical context is the structured formal layer that makes a software project analyzable.

It includes:

- the key states the system can be in
- the actions or transitions that move it between states
- predicates describing important conditions and invariants
- symbolic scenarios representing expected or forbidden behaviors
- relationships between requirements, tests, logs, and formalized behavior
- enough formal structure to support reasoning, verification, and systematic exploration

This context is useful because it supports questions that code and prose alone do not answer well:

- What behaviors are actually possible?
- Which requirements are underspecified?
- Which edge cases are not covered by tests?
- Which execution traces correspond to which formal scenarios?
- What changed semantically after a code or requirements update?
- Where are there contradictions between implementation, tests, and intended behavior?

---

## 4) Why this structure works well with LLMs

LLMs are useful for extracting and proposing formal structure, but they are unreliable when asked to invent and maintain large, globally consistent formal models in one shot.

SpecLogician is designed around this reality.

LLM-powered tools are used to:

- propose new scenarios
- refine existing scenarios
- extract predicates and transitions
- generate structured deltas
- relate informal artifacts to formal ones

But they operate on **small, local, typed artifacts**, not on one giant specification.

Each change is:

- explicit
- scoped
- structured
- machine-checkable

This aligns with what LLMs are good at:

- local reasoning
- transformation of existing artifacts
- incremental refinement
- producing structured outputs such as JSON, CLI commands, or typed edits

In this sense, SpecLogician does not ask LLMs to “solve formal methods.”  
It gives them a framework in which they can help build mathematical context safely and incrementally.

---

## 5) Agentic reasoning loop

SpecLogician sits at the center of an agentic reasoning loop for software understanding.

In this loop:

- **CodeLogician / ImandraX** translate code and logic into formal models and reasoning artifacts
- **LLM-powered agents and CLIs** propose additions, edits, and removals as structured deltas
- **program structure and navigation tools** provide architectural context
- **tests, traces, and logs** provide concrete behavioral evidence
- **documentation and requirements** provide intent-level signals

Each component contributes partial information.

SpecLogician integrates these into a single evolving formal state and uses automated reasoning to analyze that accumulated state after each change.

This creates a closed loop:

**observe → formalize → analyze → refine**

or equivalently:

**artifact → mathematical context → reasoning → improved artifact**

The important shift is that the formal model is not a static end product.  
It becomes a living semantic layer around the software project.

---

## 6) What this enables

Once a project has a maintained mathematical context, many higher-value workflows become possible.

SpecLogician can help teams:

- identify gaps and ambiguities in requirements
- discover inconsistencies between code, tests, traces, and intended behavior
- understand coverage in semantic terms, not just line or branch terms
- trace logs, test cases, and documents back to formal scenarios
- generate missing tests from behavioral gaps
- evaluate the impact of changes before they are deployed
- maintain a more authoritative, analyzable account of system behavior over time

This makes it possible to reason about software projects at a deeper level than code review, documentation review, or test execution alone.

---

## 7) Relationship to verification

Verification is an important part of SpecLogician, but it is not the whole story.

SpecLogician is not only about proving finished properties of finished models.

It is about building the formal substrate that makes verification, analysis, exploration, and refinement possible in the first place.

That is why the emphasis is on **mathematical context**:

- verification needs formal structure
- analysis needs formal structure
- test generation needs formal structure
- change-impact reasoning needs formal structure
- trustworthy AI assistance needs formal structure

SpecLogician helps create and maintain that structure from the real artifacts of software engineering.

---

## 8) Big-picture outcome

SpecLogician turns software projects from collections of loosely connected artifacts into systems with an evolving mathematical understanding of behavior.

It helps transform LLMs from:

- probabilistic assistants operating over code and text

into:

- contributors to a logic-grounded, verification-aware engineering workflow

More broadly, it makes formal methods:

- incremental
- artifact-driven
- compatible with agentic workflows
- practical for real software projects
- central to building mathematical context around software

SpecLogician is therefore best understood not just as a formal specification tool, but as a framework for creating the **mathematical context layer** that modern software projects and AI coding systems are currently missing.

---

## License

MIT — Copyright (c) 2026 Imandra. The VS Code extension carries the same license; see [`vscode-speclogician/LICENSE`](vscode-speclogician/LICENSE) for the full text. A repo-root `LICENSE` file should mirror that text.
