cff (paper), is a framework and toolchain that allows for the formal analysis of economic properties. It appears to be a remakrably powerful tool, quoting from the abstract: "it can automatically and mechanically extract all possible economic attacks on users' cryptocurrency across modeled contracts".
cff is implemented in K, we should build a backend that allows us to compile an act spec directly into a cff compatible model in K.
cff (paper), is a framework and toolchain that allows for the formal analysis of economic properties. It appears to be a remakrably powerful tool, quoting from the abstract: "it can automatically and mechanically extract all possible economic attacks on users' cryptocurrency across modeled contracts".
cff is implemented in K, we should build a backend that allows us to compile an act spec directly into a cff compatible model in K.