Formal specification of Miniscript in Alloy



Summary:

Dmitry Petukhov has created a formal specification of Miniscript using the specification language of Alloy analyzer. The spec can be used in implementing Miniscript libraries, generating test cases for implementations and checking the implementation against the spec. It can also be used in extending or amending Miniscript and exploring its properties. The Alloy spec is the first formal spec for Miniscript. The node definitions in the spec are very readable. The K framework could also be used for the task but did not have reference documentation at the time. The spec may contain mistakes and inconsistencies, and users are encouraged to submit issues on Github or communicate them in other ways.


Updated on: 2023-06-14T16:21:34.866919+00:00