TLA+ Validation Test Suite Now Available - Enabling ISO 26262 Certification for TLC

[Markus Alexander Kuppe]

Dear TLA+ Community,

We are excited to announce the availability of the Validation Test Suite for TLA+, a comprehensive testing framework that enables the use of TLC in safety-critical software development contexts, including ISO 26262 certification. The complete suite is available at: https://github.com/tlaplus/ValidationTestSuite

This validation test suite automatically generates and executes extensive test cases for TLC to help verify that it satisfies the requirements defined by Automotive Functional Safety Standard ISO 26262 for safety-critical software development. The suite was created by Dmitry Kulagin (GitHub: craft095) at NVIDIA and initially contributed by NVIDIA, which successfully used this suite to qualify TLC for their safety-critical applications. The qualification suite addresses a critical need in the TLA+ ecosystem: providing the rigorous testing and documentation required to use TLC in safety-critical contexts such as:
- Automotive systems (ISO 26262)
- Aerospace applications
- Medical devices
- Industrial control systems

By systematically exercising TLC's behavior across thousands of test cases and documenting known deviations, this suite provides the evidence base needed for tool validation in regulated industries.

This is an open-source project and we welcome contributions from the TLA+ community! Whether you're working in safety-critical domains or simply interested in systematic TLC testing, your contributions can help improve the robustness and coverage of the test suite. For questions about using the validation test suite , please feel free to reach out through the project's issue tracker.

[Andrew Helwer]

Wow, very cool and definitely a ton of work! Auto-generating TLA+ specs to systematically test TLC is something I’ve wanted for a while, and the fact that it does conformance testing against Apalache makes it even more powerful. Wonder whether Spectacle could be onboarded to this.

How are runs triggered and where are they run?

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5c622fb3-8fca-4394-aa13-4c3c8ccdf40en%40googlegroups.com.

[Markus Kuppe]

> On Sep 26, 2025, at 3:54 AM, Andrew Helwer <andrew...@gmail.com> wrote:
>
> Wow, very cool and definitely a ton of work! Auto-generating TLA+ specs to systematically test TLC is something I’ve wanted for a while, and the fact that it does conformance testing against Apalache makes it even more powerful. Wonder whether Spectacle could be onboarded to this.
>
> How are runs triggered and where are they run?

Runs are at https://github.com/tlaplus/ValidationTestSuite/actions/workflows/main.yml and triggered manually.

M.