From 78f8de9a33a17e29cda0c5a3f13e059a4efcbec8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Gr=C3=BCner?=
 <47506558+MegaRedHand@users.noreply.github.com>
Date: Fri, 17 Apr 2026 11:51:41 -0300
Subject: [PATCH] docs: add experimental features section to readme

---
 README.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index c9bdd39..336d227 100644
--- a/README.md
+++ b/README.md
@@ -132,4 +132,7 @@ Some features we are looking to implement in the near future, in order of priori
 - [Add support for pq-devnet-5](https://github.com/lambdaclass/ethlambda/issues/285)
 - [RPC endpoints for chain data consumption](https://github.com/lambdaclass/ethlambda/issues/75)
 - [Add guest program and ZK proving of the STF](https://github.com/lambdaclass/ethlambda/issues/156)
-- [Formal verification of the STF](https://github.com/lambdaclass/ethlambda/issues/272)
+
+### Experimental features
+
+We have a proof-of-concept formalization of a part of the state transition function in Lean4 in PR [#269](https://github.com/lambdaclass/ethlambda/pull/269).