TlaLink

Keeps agent-written formal models in sync with your C# code.

Overview

Formal methods such as TLA+, Dafny and P can catch concurrency bugs, lost updates and cleanup mistakes that testing misses. Until recently, writing those models took specialist skills and a lot of time. Coding agents have changed that. Mechanically translating a whole program rarely works, because the result has far too many states to check. Instead, an agent can quickly draft a small model of just the behavior you care about.

The problem TlaLink solves is keeping that model connected to the code. Code keeps changing, and a model that passed last month may no longer describe what the code does today. Without an explicit link, a passing model can give false confidence.

TlaLink is a local .NET 10 command-line tool that keeps that link explicit and checkable:

• Links live beside the model. Formal comments identify C# declarations using Roslyn IDs and explicit syntax selectors. TlaLink independently resolves both endpoints and rejects missing or duplicate counterparts. Selected source premises can also be checked, such as whether only the authorized gate outcome reaches an effect, or a supported async admission has one matching release attempt in its enclosing finally. These checks do not prove that the implementation matches the model.
• Executions are checked against the model. Where supported, TlaLink runs instrumented copies of your code and checks the recorded behavior against the model. Selected cleanup and exception paths can be observed explicitly, rather than treating scope exit as successful resource release.
• Evidence knows when it is stale. TlaLink records exactly which code, models and tool versions each result used, and reports when changes mean earlier results no longer apply. The agent then updates the model and reruns the affected checks.

Before rerunning, the agent can reassess an existing run. Changes confined to review policy or review context do not replay unchanged execution: TlaLink checks the archived execution and checker requirements, then evaluates the current reviews separately. New or changed reviews are never approved merely because the execution still applies. Adding an independent scenario likewise does not force existing scenarios to rerun: reassessment compares the selected scenario and its requirements while retaining shared execution settings and actual input-byte checks.

For larger campaigns, project reports compare explicitly selected runs with backend-specific outcomes, timings, available native metrics and outstanding reviews. Acceptance and explanation output also suggest selective next steps: revisit reviews, search an eligible TLC stage, or collect a new scenario run, without replaying unchanged execution or weakening requirements. Native proof diagnostics help localize failed or unknown obligations; explicit pinned extended-P setup and focused translation controls support repeatable campaigns. See campaign usage and setup commands. Local setup and CI share exact common tool pins; backend-specific exceptions are explicit rather than silently selecting different SDKs or JDKs. See build prerequisites.

The goal is to move from "the agent says this looks correct" to "here is the evidence, its scope and what remains unproven." You do not need to read or write TLA+, Dafny or P yourself.

TlaLink does not include an agent or hosted AI service, and it does not upload your code. It is designed for the C#/.NET toolchain.

How it works

1. Pick one question. You describe a concrete concern, such as "Can cancellation leak a credit?", and point the agent at the relevant code.
2. The agent models it and maps it to your code. It writes a small model of just that behavior and annotates both the C# and formal declarations with model-owned selectors for the selected relationships.
3. TlaLink checks the links and runs the checkers. It confirms that the annotations resolve to real C# symbols and model declarations, then runs the selected checker. Where supported, it also runs instrumented copies of your code and checks the recorded executions against the model.
4. The agent challenges its own work. It rechecks that the model matches the code, that important behavior is actually reachable, and that the checks catch the defect being investigated. Counterexamples are investigated, not tuned away.
5. You get a plain-English summary. It states what was checked, what was simplified or assumed, and what is still open. You decide whether that is good enough.

Model-owned @link annotations

Declare "annotation_version": 4 once in the root project, not in each comment. The maintained examples keep C# free of binding comments. Formal declarations use a native block comment containing @link and standard JSON. Each bind owns a unique scope::name and a compiler-resolved source selector. For example:

lock (this.gate)
{
    this.active++;
}

The formal declaration owns the same common name, independently of its native operator name:

(* @link {"bind":[{"id":"lifecycle::admit","source":{
  "symbol":"M:Lifecycle.Admit","syntax":"ExpressionStatement",
  "tokens":"this.active++;"
}}]} *)
Admit == active' = active + 1

The stable ID is lifecycle::admit; the source is selected by its Roslyn ID, not inferred from the TLA+ operator name. The same bind.source syntax works with authored PlusCal labels, Dafny declarations and P declarations. An explicit correspondence scope selects the formal inputs; a resolved pair is not proof of equivalent behavior.

Bindings alone need no executable metadata. For supported C# trace observations, add an optional capture array to the same JSON object:

{
  "bind": [{"id": "lifecycle::admit", "source": {
    "symbol": "M:Lifecycle.Admit", "syntax": "ExpressionStatement",
    "tokens": "this.active++;"
  }}],
  "capture": [{
    "binding": "lifecycle::admit",
    "actor": "1",
    "operation": "1",
    "point": "commit",
    "classification": "transition",
    "observe": ["lifecycle::active"]
  }]
}

The observed field and formal state endpoint also need a lifecycle::active binding with its field ID, guard and capture type. This excerpt is not a complete capture setup; see the Demo source, model and scope. Capture metadata lives with the formal binding. Exclusions scope correspondence, not runtime execution, input pinning or relevant argument/callee effects. See the annotation reference for the full format. Use links inspect to read a model declaration alongside its selected C# code, surrounding control/lock context and observation metadata, without changing either source. Filter by source member, attachment status or capture point, and request only the sections needed for the review. Group related attachments by C# member and optionally inline bounded, one-level selected-source callee excerpts to review multi-step cleanup paths without repeatedly fetching the same code. Agents can load the focused workspace CLI skills for source navigation, correspondence inspection and deliberate link maintenance.

What you do, and what the agent does

You	The agent
Choose the behavior worth checking.	Writes the models, properties and source selectors.
Explain intended behavior and interface guarantees.	Picks a suitable checker and runs it.
Decide whether the stated assumptions and gaps are acceptable.	Checks its model against the code and investigates failures.
Record a review decision when a project requires one.	Explains results and limits in plain English.

You should not need to read the formal models. If a result depends on an assumption you cannot judge, such as what an interface guarantees, the agent should ask rather than guess. The agent's own checks never count as your approval. The agent guidance describes what the agent is expected to do. If your agent runs from another repository, point it to that guidance explicitly.

Working with larger code

TlaLink does not model a whole program at once. For a larger system:

• Use several focused models, each answering one question.
• Cut at interfaces. Model what an interface promises, not the code underneath. If the promise is unclear, clarify the interface contract rather than relying on implementation details.
• Keep checks beside their code. Component manifests let each part of the codebase own its checks, combined into one project.
• Reuse reviewed method summaries. Small TLA+ relations let caller models omit helper internals. Source-pinned agent inspection supports the abstraction; caller results remain conditional on it.
• Only re-check what changed. With a declared result store, completed TLC searches are reused while their models and configurations are unchanged, like an incremental build. Expensive searches can run once, separately, with a larger budget. See reusing results. Reassess existing runs with accept before executing again: review-only document changes require fresh reviews, not fresh native execution.

Combining checks in one project is for organization and repeatability. It does not prove that the separate results add up to a system-wide guarantee. Larger projects also take real effort: some searches may hit their limits, and some questions may stay open for review.

Getting started

Prerequisites

• Windows x64 or Linux x64.
• The .NET 10 SDK selected by global.json.
• PowerShell 7 for repository scripts.

Build and test

From the repository root:

dotnet build .\TlaLink.sln
dotnet run --project .\tests\TlaLink.Tests\TlaLink.Tests.csproj -- . --core

These need no formal-methods tools. The checkers themselves are set up separately, only when you need them; see the setup instructions.

Package as a .NET tool

dotnet pack .\src\tlalink\TlaLink.csproj --configuration Release --output .\dist

The resulting TlaLink NuGet package exposes dotnet tlalink through a consumer's local tool manifest. Commit that manifest and use dotnet tool restore in build setup. No package is published by this command, and native checkers are not bundled. See installation and package tests.

Provision pinned prebuilt checkers explicitly during setup:

dotnet tlalink toolchain restore --directory .\.tools --timeout 600

This installs or checks the pinned JDK, TLC, Dafny, Apalache and P compiler. Repeat runs check complete file contents; offline reuse and guarded repairs are supported. It never installs tools during analysis, upgrades pins or changes proofs or approvals. See native tool restore.

Use symbol lookup to discover exact C# declaration IDs, resolve source positions, find references/call sites or inspect one member without adding annotations or reading a whole inventory.

First steps

Open this repository alongside your code in your coding agent, and give it access to the relevant sources and a shell. Then ask it to:

1. Check setup and walk you through the small C# example and its TLA+ model.
2. Run the lanes scenario in the workflow example, which checks a recorded C# execution against a model.
3. Help you choose one concrete question about your own code.

Examples

Example	Shows
Demo and its model	Linking C# code to a TLA+ model.
Workflow	A repeatable project, including a recorded-execution check.
Components	The project layout in its smallest form, with shared inputs and time limits.
Evidence stages	C# regressions and Dafny proofs in one project.
Apalache	Symbolic TLA+ type, bounded safety and induction checks.
Integrated bindings	Comparing C# calls with verified Dafny results.
P	Linking C# to a P state machine checked with PChecker.
Dispatcher campaign	A shared C# lifecycle across the supported backends, with defect controls and measured limitations.

Each example project uses the same layout: a small root tlalink.project.json that selects component.json files kept beside the code they check. The examples overview describes each one and the tools it needs. The examples are synthetic demonstrations, not policies for your system.

Supported tools

TlaLink runs existing, established tools rather than replacing them. You only need the ones your chosen checks use.

Tool	Used for
Roslyn	Resolving the C# side of the links.
TLA+ tools (SANY, PlusCal, TLC)	Parsing TLA+ models, exploring their states and checking recorded executions.
Apalache	Symbolic checking of TLA+ safety properties.
Dafny	Proving algorithmic contracts and modeled safety invariants, including arbitrary finite histories; comparing selected C# calls with verified results.
P	Checking asynchronous state-machine models and logs.

Choose by the question, not a fixed language ranking. General safety proofs, interleaving exploration and eventual-progress checks need different evidence; none automatically proves the linked C#. The selection guide compares modeling fit, checker guarantees and current integration limits.

Limitations

• A passing model is not proof that the C# is correct. Checkers verify the model. How well the model matches the code depends on the mapping, the agent's checks and any reviews.
• Linked does not mean correct. TlaLink confirms that annotations point at real code and model elements, not that they describe the code accurately.
• Execution checks cover what ran. A recorded execution that matches the model shows that one run fits; it does not cover every possible run.
• Incomplete is not passed. Timeouts, missing tools and partial searches are reported as incomplete.
• Results can go stale. When code or models change, TlaLink reports whether earlier evidence still applies.

A good summary keeps these distinctions visible rather than reporting a single "verified" badge. See the design for the precise limits of each kind of check.

Documentation

• Reference: setup, commands, annotations, file formats and testing.
• Design: architecture and what each kind of evidence does and does not show.
• Agent guidance: how agents should build models and operate the tool.
• Security: reporting vulnerabilities.

If you use a coding agent, its own data handling depends on its configuration.

License

TlaLink is licensed under the MIT License.