diff --git a/doc/src/introduction.md b/doc/src/introduction.md
index 4cbfa9aa..97cd8ebf 100644
--- a/doc/src/introduction.md
+++ b/doc/src/introduction.md
@@ -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  -->
diff --git a/doc/src/lean.md b/doc/src/lean.md
index 8a98db59..d8ad5026 100644
--- a/doc/src/lean.md
+++ b/doc/src/lean.md
@@ -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:
 
diff --git a/doc/src/type_checking.md b/doc/src/type_checking.md
index ce6d6b39..cf88fecc 100644
--- a/doc/src/type_checking.md
+++ b/doc/src/type_checking.md
@@ -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.