From 3fddea7dcfc716fc50fd671521cfd9ac9e423a65 Mon Sep 17 00:00:00 2001 From: David Terry Date: Tue, 14 Nov 2023 10:45:19 +0100 Subject: [PATCH] readme: update intro --- README.md | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 4d69c4a5..29e82ccc 100644 --- a/README.md +++ b/README.md @@ -1,20 +1,16 @@ # Act -This project is an effort by several groups working on formal methods for -Ethereum smart contracts, aiming at creating a simple but effective language -to write formal specification. -It extends on the previous -[Act](https://github.com/dapphub/klab/blob/master/acts.md) project. - -Some general features it hopes to achieve are: -- Simple structure and logic. -- Support writing properties on a high level (closer to Solidity/Vyper) as - well as on the machine level. -- Cross-tool communication: Different tools might be able to generate - different knowledge and use the specification language to exchange - information. -- No attachment to a particular logic. If a tool wishes to support certain - expressions, extensions can be written. +Act is a formal specification language, designed to allow for the construction of an exhaustive, +mathematically rigorous description of evm programs. Act allows diverse toolchains to interoperate +on a single specification, with each generating and exchanging different kinds of knowledge. It has +a built-in analysis engine that can automatically prove properties about the specification itself, +as well as an integrated symbolic execution engine (based on hevm) that can prove equivalence +between a specification and a given bytecode object. Finally, specifications can be exported into +higher level reasoning tools (e.g. theorem provers, economic analysis tooling), allowing for the +verification of properties of almost arbitrary complexity, all with a proof chain right down to the +bytecode level. + +It extends on the previous [Act](https://github.com/dapphub/klab/blob/master/acts.md) project. More in depth documentation can be found in [The Act Book](https://ethereum.github.io/act/).