syumei
Building a Mini Lean 4 from Scratch: Implementing a Theorem Prover in Rust
I Rebuilt an AI Gateway in Rust. It Became 41× Faster
Getting Started with Lean 4: Proofs as Code for Real Developers
Succinct Offers ZK Verification to Chainlink CCIP 2.0 Users
Re:I Tried to Verify Rust OSS with Lean 4 and Found Many Bugs
on Monday October 19, 2026 @03:09PM (#50156602)
Thanks for the feedback! I should have explained the process more clearly. I first formalized security properties in Lean 4 (automatically extracted from Rust code) and attempted to prove them. All the bugs mentioned in the article were discovered by investigating failed proof attempts, and I then confirmed them with concrete tests against the original projects. So the Lean proof attempts came first, not the tests. I'll clarify this in the article!
I Tried to Verify Rust OSS with Lean 4 and Found Many Bugs
Proving Rust Web Application Correctness with Lean 4
Can a coding agent formally verify what real-world Rust code does, in Lean 4?
I5h: Build a Rust Web App and Prove Its Behavior with Lean 4
Ask HN: Can we translate normal Rust (axum) to Lean 4 without restrictions?
I'm trying to build a web app in Rust using axum, and am thinking whether I can export that Rust code to Lean4 so that I can verify business logic or security properties.I first tried Aeneas, but it can only work for restricted grammer and structurs that are hard to review (it even doesnt look like Rust).For example, when I want to write:``` fn find_post(ps: &[Post], id: u64) ->...
How JWT Authentication Works
Building a Browser Without V8: What Broke, and What Worked
Think Like an Attacker: CI/CD Security in the AI Era
$1,500 AI System Prompt Leak: Using This Burp Suite Configuration
Cilfi: Automatic Function Identification in .NET Binaries
How to Become an Ethical Hacker – HTTP Request Tampering
I built a browser and HTTP client together from scratch for pentesting
Top 20 AI Agent Pen-Testing Tools for 2026: The Ultimate Guide
Grand Theft Auto VI Hype Leads to Malware
CrowdStrike Announces Agentic Identity Provider
Malware Analysis in the Age of AI: What Still Requires Human Skill?
Hacking Cable: AI in post-exploitation operations
CVE-Bench evaluates the capability of AI agents to exploit web vulnerabilities
SoC Analysts Read Firewall Logs: What You Are Expected to Know
Re:Do We Still Need Burp Suite for Web Security Testing?
on Monday September 07, 2026 @12:56PM (#49600411)
I've heard of Vulnetic, and it looks quite cool, though I feel it's a bit expensive for individual users (probably fine for companies)