CINXE.COM
<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"> <meta http-equiv="X-UA-Compatible" content="IE=edge"> <meta name="viewport" content="width=device-width, initial-scale=1"> <link rel="stylesheet" href="/assets/main.css"> <link rel="alternate" type="application/rss+xml" title="alloy" href="/feed.xml"> </head> <body> <header class="site-header" role="banner"> <div class="wrapper"> <a class="site-title" href="/">alloy</a> <nav class="site-nav"> <input type="checkbox" id="nav-trigger" class="nav-trigger" /> <label for="nav-trigger"> <span class="menu-icon"> <svg viewBox="0 0 18 15" width="18px" height="15px"> <path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/> <path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/> <path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/> </svg> </span> </label> <div class="trigger"> <a class="page-link" href="/about.html">about</a> <a class="page-link" href="/applications.html">uses</a> <a class="page-link" href="/book.html">book</a> <a class="page-link" href="/community.html">community</a> <a class="page-link" href="/documentation.html">docs</a> <a class="page-link" href="/download.html">download</a> <a class="page-link" href="/models.html">models</a> </div> </nav> </div> </header> <main class="page-content" aria-label="Content"> <div class="wrapper"> <div class="home"> <div style="float:right;width:250px; margin-left:20px;"> <img style="float:right"src="/image/cover.jpg"/> </div> <h2 id="alloy">Alloy</h2> <p>Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks. This site provides language documentation, tool downloads, and a repository of links to case studies and applications. As the open source community grows, this site will also provide access to extensions of the Alloy Analyzer, and tools built on top of it and on top of Kodkod, its model finding engine.</p> <h2 id="last-release">Last release</h2> <p>The last release to date (2025/01/09) is <a href="https://alloytools.org/download.html">Alloy 6.2.0</a> .</p> <h2 id="alloy-6">Alloy 6</h2> <p>Alloy 6 is a major revision w.r.t Alloy 4, that adds mutable state, a temporal logic and accompanying solvers as well as an improved Visualizer. Specifying the behavior of systems gets easier in many cases.</p> <p><strong>Compared with pre-6 versions of Alloy, this version comes along with some important syntactic changes. Please read the <a href="alloy6.html">this page</a> in detail to learn more.</strong></p> <h2 id="learning-alloy-6">Learning Alloy 6</h2> <p>2025/02/19: <a href="https://practicalalloy.github.io/">Practical Alloy – A hands-on guide to formal software design</a> is a new (draft) online book on Alloy 6+, by Alcino Cunha, Nuno Macedo, Julien Brunel and David Chemouil.</p> <div style="display:none">SHA for JDEPLOY 10386f1b4531f26c1b97138791151464bb6f66b5a1301438db9f29437d0d236d</div> <h2 class="page-heading">announcements</h2> <ul class="post-list"> </ul> </div> </body> </html>