Update security-tools.mdx (#1594)

Add description of Certora security.

Author: ilyaCertora

docs/tools/developer-tools/security-tools.mdx

@@ -16,3 +16,7 @@ A static code analysis tool built to assist Soroban developers and auditors in i
 Almanax is an AI security engineer designed to help teams prevent hacks.
 
 Almanax uses LLMs to identify complex security vulnerabilities in both smart contracts and conventional code. It also integrates with CI/CD pipelines to automatically flag issues before code reaches production.
+
+### [Certora Sunbeam](https://docs.certora.com/en/latest/docs/sunbeam/index.html)
+
+Sunbeam is a formal verification tool developed by Certora for Soroban smart contracts on the Stellar blockchain. Designed specifically for WebAssembly (Wasm) bytecode, Sunbeam verifies the deployed contract code—not just the Rust source—eliminating the need to trust the Rust compiler. Developers write correctness properties using a lightweight spec language embedded in Rust, and Sunbeam rigorously checks that the compiled Wasm upholds those properties.