Merge pull request #174 from ethereum/better-readme

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/).