Since we introduced Aegis, the formal verification tool for Starkware’s Cairo language, two years ago, the framework has seen several versions of Cairo, of Starknet, and of Lean (the theorem prover powering the tool) go by and change the underlying code base. It’s time to recap what we achieved in this time and what’s yet to come.
Since we base our verification on Cairo’s intermediate representation Sierra, it was most important to keep up to date with the newest additions to Sierra. Sierra’s atomic instructions are called libfuncs. In the recent version we added Aegis support for the use various new libfuncs, such as:
Signed integer types and the libfuncs providing arithmetic operations on them
Casts between various unsigned and signed integer types
Bounded integer types, which offer a generalization of fixed-bitwidth integer types, with a statically guaranteed lower and upper bound
Support for the new bytes31 type, which packs 31 bytes into a single felt
We’ve used these additions to cover new ground in the attempt to fomally verify as much of Cairo’s core library (corelib) as we need for our purposes. Part of porting our verification of corelib along different Cairo versions was to reimplement the representation of fixed-bitwidth integers with the newly build Lean library for bitvectors. These allow us to solve various verification goals with bitblasting tactics that weren’t available to us when we still represented those types in a more algebraic way.
Various verification efforts showcase the use of Aegis, for example
We verified our WadRay fixed-point arithmetics library (https://github.com/lindy-labs/wadray_verification)
As a proof of concept for Starkware, we verified Starkware’s own implementation of fractions in Cairo (https://github.com/lindy-labs/fraction_verification)
We verified the production code of the controller module of our own Opus contracts (https://github.com/lindy-labs/opus_contracts_verification)
In the future we hope that further proof automation will make the use of Aegis even easier and that the Cairo ecosystem will consist of more code that’s been verified using the tool. Immediate future projects could include
Verifying the core library’s implementation of byte arrays
Improving the interplay between types that are represented in Lean by bitvectors and types that are represented algebraically using the
ZModdatatypeVerifying other components of Opus and of other popular smart contracts
Adding Aegis support for polymorphic verification of polymorphic functions
As it stands, the Aegis project is on hold but OSS contributions are always welcome!
