diff --git a/README.md b/README.md
index e36e61da..1a2dcb14 100644
--- a/README.md
+++ b/README.md
@@ -409,6 +409,7 @@ Many thanks to the ~100 contributors including [@corbpage](https://twitter.com/c
 * [Piet](https://piet.slock.it) - A visual Solidity architecture analyzer
 * [Smack My Contract](https://smackmycontract.xyz/) - Web3 Security Scanner Aggregator
 * [EVMole](https://github.com/cdump/evmole) - Extracts function selectors from EVM bytecode, even for unverified contracts
+* [Kontrol](https://github.com/runtimeverification/kontrol) - Formal verification of Solidity smart contracts through Foundry property tests
 
 ### Monitoring
 * [Moralis Streams API](https://docs.moralis.io/streams-api) - Stream real-time on-chain events to your webhook from multiple EVM blockchains.
diff --git a/README_Chinese.md b/README_Chinese.md
index 8d894d46..f7686b7a 100644
--- a/README_Chinese.md
+++ b/README_Chinese.md
@@ -333,6 +333,7 @@ https://github.com/ConsenSys/ethereum-developer-tools-list/pull/70
 * [Awesome Buggy ERC20 Tokens](https://github.com/sec-bit/awesome-buggy-erc20-tokens) -受影响的代币中ERC20智能合约中的漏洞的集合
 * [Free Smart Contract Security Audit](https://callisto.network/smart-contract-audit/) - Callisto Network提供的免费的智能合约安全审核
 * [Piet](https://piet.slock.it) - 可视化Solidity体系结构分析器
+* [Kontrol](https://github.com/runtimeverification/kontrol) - 通过 Foundry 属性测试对 Solidity 智能合约进行形式验证 
 
 ### 监控方式
 * [Alethio](https://aleth.io/) - 一个先进的以太坊分析平台，提供实时监控，洞察和异常检测，令牌指标，智能合约审计，图形可视化和区块链搜索。还可以探索以太坊去中心化交易所的实时市场信息和交易活动。
diff --git a/README_Japanese.md b/README_Japanese.md
index 03542157..4d777f53 100644
--- a/README_Japanese.md
+++ b/README_Japanese.md
@@ -211,6 +211,7 @@ Ethereum開発で利用可能なツール、コンポーネント、パターン
 * [Manticore](https://github.com/trailofbits/manticore) - スマートコントラクトとバイナリのためのSymbolic executionツール  
 * [Solidity security blog](https://github.com/sigp/solidity-security-blog) - 既知の攻撃手法と一般的なアンチパターンの包括的なリスト  
 * [Awesome Buggy ERC20 Tokens](https://github.com/sec-bit/awesome-buggy-erc20-tokens) - ERC20トークン・スマートコントラクトの脆弱性コレクション 
+* [Kontrol](https://github.com/runtimeverification/kontrol) - Foundryのプロパティテストを通じたSolidityスマートコントラクトの形式的検証
 
 ### モニタリング
 * [Neufund - Smart Contract Watch](https://github.com/Neufund/smart-contract-watch) - 多くのスマートコントラクト、トランザクションを監視するためのツール
diff --git a/README_Korean.md b/README_Korean.md
index a8a8cd79..d4aa4e7f 100644
--- a/README_Korean.md
+++ b/README_Korean.md
@@ -284,6 +284,7 @@
 * [솔리디티 보안 블로그(Solidity security blog)](https://github.com/sigp/solidity-security-blog) - 알려진 공격 백터(vectors)와 일반적인 안티패턴(anti-patterns) 종합 리스트 입니다.
 * [어썸 버기 ERC20 토큰(Awesome Buggy ERC20 Tokens)](https://github.com/sec-bit/awesome-buggy-erc20-tokens) - 토큰에 영향을 주는 ERC20 스마트 컨트렉트의 취약성 모음 입니다.
 * [Free Smart Contract Security Audit](https://callisto.network/smart-contract-audit/) - Callisto 네트워크의 무료 스마트 컨트렉브 보안 감사(audits) 입니다.
+* [Kontrol](https://github.com/runtimeverification/kontrol) - Foundry 속성 테스트를 통한 Solidity 스마트 계약의 형식 검증.
 <a name="모니터링"></a>
 ### 모니터링
 * [노이펀드(Neufund) - Smart Contract Watch](https://github.com/Neufund/smart-contract-watch) - 스마트 컨트렉트와 거래의 수를 모니터하는 도구 입니다.
diff --git a/README_Spanish.md b/README_Spanish.md
index f024f322..6b7b1799 100644
--- a/README_Spanish.md
+++ b/README_Spanish.md
@@ -346,6 +346,7 @@ Muchas gracias a los ~100 contribuidores, incluidos [@corbpage](https://twitter.
 * [Awesome Buggy ERC20 Tokens](https://github.com/sec-bit/awesome-buggy-erc20-tokens) - una colección de vulnerabilidades en contratos inteligentes ERC20 con tokens afectados.
 * [Auditoría de seguridad de contrato inteligente gratuita](https://callisto.network/smart-contract-audit/) - Auditorías de seguridad de contrato inteligente gratuitas de Callisto Network.
 * [Piet](https://piet.slock.it) - un analizador visual de arquitectura de Solidity.
+* [Kontrol](https://github.com/runtimeverification/kontrol) - Verificación formal de smart contracts escritos en Solidity mediante tests de propiedades en Foundry.
 
 ### Monitoreo
 * [Alethio](https://aleth.io/) - una plataforma de análisis avanzada de Ethereum que proporciona monitoreo en vivo, información y detección de anomalías, métricas de tokens, auditorías de contratos inteligentes, visualización de gráficos y búsqueda de blockchain. También se puede explorar la información de mercado en tiempo real y las actividades comerciales en los intercambios descentralizados de Ethereum.