microsoft/tlalink

microsoft/tlalink

Description: Links TLA+/Plang/Dafny with sources for managing correctness proofs

Language: C#

License: MIT

Stars: 0

Forks: 0

Open issues: 1

Created: 2026-10-25T09:51:51Z

Pushed: 2026-10-27T06:47:47Z

Default branch: main

Fork: no

Archived: no

README:

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 in your code. The agent annotates the C# to show which code

each model step and variable represents. TlaLink checks that every link still resolves to real code and model declarations.

• Executions are checked against the model. Where supported, TlaLink runs

instrumented copies of your code and checks the recorded behavior against the model.

• 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.

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 the C# to show which code each model step and variable represents. 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.

The project declares the annotation version once; it is not repeated in source. The mapping lives in your source as short @link annotations. For example, this says the increment under the lock is the model step Admit:

lock (this.gate)
{
/* @link
step Admit justification=lock actor="1" operation="1" point=commit classification=transition observe=active;
*/
this.active++;
}

What you do, and what the agent does

| You | The agent | |---|---| | Choose the behavior worth checking. | Writes the models, properties and code annotations. | | 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](AGENTS.md#model-authoring-and-self-checks) 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](examples/Components/README.md)

let each part of the codebase own its checks, combined into one project.

• 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](REFERENCE.md#reusing-completed-tlc-results).

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](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](REFERENCE.md#requirements-and-build).

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](examples/Demo.cs) and its [TLA+ model](examples/Demo.tla). 2. Run the lanes scenario in the [workflow example](examples/Workflow/tlalink.project.json), which checks a recorded C# execution against a model. 3. Help you choose one concrete...