Skip to content

tech report with metatheory link #222

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
anjapetkovic merged 1 commit into from
May 4, 2026
Merged

tech report with metatheory link #222

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions doc/src/introduction.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ act provides two main verification backends that work with the same specificatio
<!-- have ERC20 example already here? -->

Further key capabilities of act:
<!-- mention formally defined semantics + type safety + soundness -->
- **The semantics of act is fully formally defined.** Type safety and soundness are proven in detail. <span style="color:green">A full tech report will be available shortly.</span>
<!-- mention formally defined semantics + type safety -->
- **The semantics of act is fully formally defined.** Type safety is proven in detail. A full technical report with all definitions and proofs is available [here](https://arxiv.org/abs/2604.02955).
<!-- talk about language agnostics -->
- **act is language agnostic**: Conceptually, act could support conformity of spec and implementation written in all programming languages that compile to EVM bytecode. Currently (in v0.2.0), Solidity and Vyper are supported.
<!-- loops -->
Expand Down
2 changes: 1 addition & 1 deletion doc/src/lean.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ Make sure to run `lake update` in the `lib/` directory and also in your project
## act Export

Calling `act lean ...` will generate a Lean file that encodes the contract as a state transition
system, following the formal value semantics given in the <span style="color:green">tech report (to be available shortly).</span>
system.

The generated file begins with imports and opens the relevant namespaces:

Expand Down
2 changes: 1 addition & 1 deletion doc/src/type_checking.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Type-Checking

act's type-checking process ensures that specifications are both syntactically correct and semantically sound. It combines traditional static type-checking with semantic verification using SMT solvers. Type safety is proven in detail. <span style="color:green"> A full tech report will be available shortly. </span>
act's type-checking process ensures that specifications are both syntactically correct and semantically sound. It combines traditional static type-checking with semantic verification using SMT solvers. Type safety is proven in detail. A full technical report with all definitions and proofs is available [here](https://arxiv.org/abs/2604.02955).

The type-checker implements the formal typing judgments defined in act's type system. It verifies that all expressions are well-typed according to typing rules, which take storage declarations, interface parameters, and local bindings into account.
The type-checker proceeds systematically: it first type-checks each contract's constructor, memorizing the constructor's storage declarations, then type-checks each transition against the updated environment. This ensures type consistency across the entire specification and catches errors like type mismatches, undefined variables, and invalid operations before proceeding to the verification backends.
Expand Down
Loading