Requirements analysis: catching requirement bugs before they become code https://lobste.rs/s/ycbrru #formalmethods
https://kiro.dev/blog/deep-spec-analysis/
formalmethods
What Happens to Software When Proof is Cheap? https://lobste.rs/s/r8epo9 #video #formalmethods #vibecoding
https://www.youtube.com/watch?v=oSHVPvM56sA
A sufficiently comprehensive spec is not (necessarily) code https://lobste.rs/s/u1fem9 #formalmethods #vibecoding
https://buttondown.com/hillelwayne/archive/a-sufficiently-comprehensive-spec-is-not/
A blueprint for formal verification of Apple corecrypto https://lobste.rs/s/7crjja #cryptography #formalmethods
https://security.apple.com/blog/formal-verification-corecrypto/
Announcing Isabelle support for SAW https://lobste.rs/s/xha7ff #cryptography #formalmethods
https://www.galois.com/articles/announcing-isabelle-support-for-saw
Introduction to Formal Verification with Lean (Part 1) via @nemin https://lobste.rs/s/ymnnmv #formalmethods
https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)
hax: A Rust verification tool https://lobste.rs/s/rdbc5p #formalmethods #rust
https://github.com/cryspen/hax
Automatic Programming Should Be More Like SQL https://lobste.rs/s/oh7zna #formalmethods #plt #vibecoding
https://stng.substack.com/p/automatic-programming-should-be-more
Building an Unverified Compiler with Agents https://lobste.rs/s/fkxdc8 #formalmethods #plt #vibecoding
https://www.basis.ai/blog/verified-compiler/
Signal Shot: a project to verify the Signal protocol and its Rust implementation using Lean https://lobste.rs/s/jnl6e7 #cryptography #formalmethods #security #vibecoding
https://leodemoura.github.io/blog/2026-4-20-signal-shot-the-platform-is-ready/
Validating Hare’s Sort Module using Symbolic Execution via @RunxiYu https://lobste.rs/s/yoq0e6 #formalmethods #plt
https://notes.8pit.net/notes/y7n8.html
Verifying (simple) C in Isabelle/HOL with AutoCorres via @abnv https://lobste.rs/s/pw3qa0 #c #formalmethods
https://blueberrywren.dev/blog/isabelle-autocorres-tut/
LemmaScript: A Verification Toolchain for TypeScript via Dafny https://lobste.rs/s/4tuujf #formalmethods
https://midspiral.com/blog/lemmascript-a-verification-toolchain-for-typescript/
The changing role of finite-state model checking by @ahelwer https://lobste.rs/s/3hoiw8 #formalmethods #testing
https://ahelwer.ca/post/2026-08-24-finite-state-future/
Interested in theoretical cryptography and/or formal methods? Boston University is hosting a summer school on Universally Composable Security and the EasyUC framework for formalizing UC models and proofs.
The school is from August 11 - 14, 2025. Registration is free, and we're supporting both in person and Zoom participation.
For more information and to register, visit:
I am hiring!
I have a fully funded PhD position available for someone with an interest in logic and statistics, at Delft University of Technology (Netherlands).
Application deadline: 31 August 2025
#AcademicJobs #AcademicMastodon #GetFediHired #AcademicJob #SymbolicAI #Statistics #AI #ConstraintProgramming #CombinatorialOptimisation #SensitivityAnalysis #FormalMethods #CombinatorialOptimization #Delft #TUDelft #AcademicChatter
A Rust-to-Lean verification pipeline with AI provers: An experience report https://lobste.rs/s/g2bzt2 #formalmethods #rust #vibecoding
https://arxiv.org/html/2605.30106
Domain-specific hyperspecialization (for SAT) https://lobste.rs/s/cccby7 #formalmethods #vibecoding
https://c.mov/lymphosat/
How we used Quint to find over 10 bugs in SQLite while hardening Turso https://lobste.rs/s/maqmo2 #databases #formalmethods
https://turso.tech/blog/how-we-used-quint-to-find-over-10-bugs-in-sqlite
On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications https://lobste.rs/s/ukw5wf #formalmethods #testing #vibecoding
https://proofsandintuitions.net/2026/05/18/property-based-testing-specifications/
Functional Algorithms, Verified https://lobste.rs/s/lqthae #pdf #formalmethods #plt
https://www21.in.tum.de/teaching/fds/SS21/assets/book-draft.pdf
"Why not just use Lean?" https://lobste.rs/s/d27llp #formalmethods
https://lawrencecpaulson.github.io/2026/04/23/Why_not_Lean.html
Illegal vs Unwanted States https://lobste.rs/s/szrxqe #formalmethods
https://buttondown.com/hillelwayne/archive/illegal-vs-unwanted-states/
Giving LLMs a Formal Reasoning Engine for Code Analysis https://lobste.rs/s/fu9wcm #formalmethods #vibecoding
https://yogthos.net/posts/2026-04-08-neurosymbolic-mcp.html