Asmeta is a framework for the Abstract State Machines (ASMs) formal method. It is composed of different tools for performing different validation and verification activities.

It is based on the definition of a metamodel for ASMs. For the metamodel semantics, we adopt the ASMs semantics given in the ASM book.

You can find information on how to download and install the tools.

The documentation about the language and the tools can be found here.

The source code can be found in the github repository https://github.com/asmeta/asmeta.

News

Oct 25 new release 25.09 with several improvements - including a choose with infinite domain
Jun 25 new papers at ABZ2025 and NFM2025
Jun 25 new release 25.06 with several improvements - including undef as monitored value
Mar 25 new release 25.03 with several improvements - including a new pick command for avalla (more soon)
Sep 24 we will have a tutorial on asmeta at FM24
Jun 24 new release 24.06 with several improvements
Apr 24 new relaese 24.04 with many bug fixes is now available, including lazy evaluation
Mar 23 new relaese 23.03 with several bug fixes is now available