Post

act is a formal specification language with a range of capabilities, one of which is proving that EVM bytecode matches a human-readable spec. Think of it as a way to mathematically guarantee that a contract does exactly what it claims to do.

Building under one umbrella means our work streams reinforce each other. We collaborate across teams from the start and apply our tools wherever they add value. Two recent cases with Solidity and Fe show what that looks like in practice.

Example 1: Core Solidity
 We wrote a simple contract in solcore along with its act specification & tried to prove they were equivalent. act said they weren't. After some digging we discovered that constructors were payable by default, which was unintended.