Tesota 0.1.0-alpha.9

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.8

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.7

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.6

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.5

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.4

A coding agent that ends every run with a receipt. When the agent finishes, Tesota proves the change where it can, tests it where it can't, and writes a receipt that says what was verified and what wasn't. This alpha is the first public release. Most of it was written by Tesota itself, through tesota -p, reviewed by a model of another family, and reviewed by hand.

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify <file> --repo sequelcore/tesota.

New

• Documentation rewritten for this release:

  • a model checking guide for readers new to TLA+;
  • a reference of all 33 proved rules;
  • a glossary;
  • a changelog;
  • NOTICE built from what the binary actually contains.

  tesota --help lists the commands. (#683, #684)

• A new look.

  • The input is a full-width band, and so are your messages in the conversation. The shell opens with a compact header.
  • Tesota's mark is redrawn: Olneya tesota, the desert ironwood, a nurse tree that shelters young saguaros.
  • It blooms only when a request is verified, the same rule the receipt's text follows. Nothing moves while the agent works, and without color only its silhouette shows. (#671)
  • The header is compact: a narrower tree, 11 columns by 3 rows. (#678)
  • Every list marks its selected row with a full-width band: slash commands, pickers and questions. (#673)

• Usage panel. /usage shows how much each account has left: a meter per limit window, when it resets, and warning colors.

  • /accounts opens the same dialog on its Accounts tab, to sign in again or remove an account.
  • Claude's limits come from Claude Code's own report. Tesota never reads Claude Code's credentials.
  • ChatGPT's come from the Codex sign-in. The newer OpenAI sign-in doesn't report them, and the panel says so.
  • It opens at once on saved readings and marks the account this session draws on. (#677)

• Model graphs.

  • When TLC checks a TLA+ model, Tesota keeps the graph it actually explored, in the same run that produced the evidence.
  • The transcript previews it. /graph opens it full-screen, grouped by variables, with every broken rule marked, and the failing run as the only real execution.
  • o opens the same graph in your browser, as one self-contained HTML file beside the session: no server, no network.
  • The page says what went wrong in plain words, with the broken rule's own text from the model. It's generated from TLC's data, never drawn by the model. (#592, #593, #662, #665)

• Resume a headless run with your answer. When an agent asks you something in tesota -p, the run says how to answer: tesota -p --resume <id> "<answer>", or -c for the latest session. The same request continues from the same base. Your answer is recorded as a clarification, never as permission. (#651)

• Several accounts. Choose a session's account like a model: claude-code@<name>/…, openai-codex@<name>/…. tesota accounts add signs one in, in one step. (#636, #642)

• Test weakening, named. When a test edit may weaken evidence, the receipt says how: a loosened assertion, a skipped test, a new mock of the code under test. (#646)

• One block per request: a live ledger while it works, which becomes the receipt. The running check shows its command and elapsed time. (#591, #616)

• A scratch folder per session, which the agent's instructions name, so a harmless temporary file never stalls a run. (#653)

More honest

• "Failed" means a check ran and showed the change wrong.

  • A check that couldn't run, timed out, checked nothing or is stale is a gap, so the run is incomplete, never failed.
  • One proved rule decides this for proofs, tests and design models alike. (#685)

• An exported receipt states what happened:

  • COMPLETED, FAILED or CANCELLED;
  • tesota receipt --json refuses an incomplete run, or a commit that doesn't hold exactly what the checks saw. (#685)

• Each proof says what it covers. LemmaScript models numbers as exact, not floating-point, and the receipt says so under each proof. (#685)

• "Verified" now means evidence.

  • A run ends Completed, verified only when a check passed, every changed file is proved or tested and exercised, and nothing is missing.
  • Before, it meant "nothing needs you", so a run with no evidence at all could say "verified".
  • Now a run says incomplete, unverified, or plain Completed (nothing changed), and the receipt's summary never contradicts it. (#668)

• An agent's unanswered question ends the run as incomplete, and verifies what changed, never as a quiet pass. (#599)

• Evidence whose file changed before the receipt reads as stale, not as passed. (#617)

• A stopped run gets an inventory of what changed. A run whose process died is recorded as interrupted, and nothing is invented. (#599)

• A request is credited only for its own commits when the history moves under it. (#599)

• A receipt made from source names its commit (0.1.0-alpha.4+<commit>), not just the release. (#639)

• A test runner's pass counts only when a target test ran. (#615)

Fixed

• Signing in with a browser works on Windows.
  • The sign-in page opens on its own.
  • Its link is shown whole, so it can be clicked, and c copies it.
  • Tesota says plainly when the browser didn't open. (#676)
• A resumed headless run continues on the model it last ran on, account included. --model still overrides it, and says so. (#675)
• Floor refusals are held to their effect and shown at the end. (#622)
• A writing subagent is kept off every branch but its own. (#619)
• A read-only session verifies nothing. (#585)
• The change side runs in the base's worktree, and Jest gets exact test paths. (#618, #620)
• A stopped run no longer leaves a stuck Git process running. (#648)
• A session whose model sent malformed edit arguments resumes again. (#657)
• Multi-line text pasted into a question keeps its line breaks as spaces. (#624)
• /resume reopens a session that worked in the folder's checkout. (#625)

Tesota 0.1.0-alpha.3

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.2

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.

Tesota 0.1.0-alpha.1

Install with the scripts in docs/get-started/install.md. Check a binary's provenance with gh attestation verify --repo sequelcore/tesota.