StarMalloc: verified memory allocator https://lobste.rs/s/jpfyd6 #compsci #formalmethods #security
https://dl.acm.org/doi/10.1145/3689773

100 years of Zermelo’s axiom of choice: What was the problem with it? https://lobste.rs/s/kbcp5p #formalmethods #math
https://research.mietek.io/mi.MartinLof2006.html

Writing a Verified Postfix Calculator in Ada/SPARK https://lobste.rs/s/uwhv3o #formalmethods #programming
https://pyjarrett.github.io/2025/06/10/postfix-calculator.html

Proving completeness of an eventually perfect failure detector in Lean4 https://lobste.rs/s/adl5af #distributed #formalmethods
https://protocols-made-fun.com/lean/2025/06/10/lean-epfd-completeness.html

Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library https://lobste.rs/s/p8uq6e #c #formalmethods #rust
https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/

Passing of Jean-Raymond Abrial https://lobste.rs/s/hao2zr #formalmethods
https://en.wikipedia.org/wiki/Jean-Raymond_Abrial

Lightweight Diagramming for Lightweight Formal Methods https://lobste.rs/s/mgdqwx #formalmethods
https://blog.brownplt.org/2025/06/09/copeanddrag.html

NVIDIA ISO-26262 SPARK Process https://lobste.rs/s/mkivgh #formalmethods #practices #release
https://nvidia.github.io/spark-process/

What Works (and Doesn't) Selling Formal Methods

https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods

Discussions: https://discu.eu/q/https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods

AI is a gamechanger for TLA+ users https://lobste.rs/s/mp34xp #formalmethods #vibecoding
https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/

Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs | MongoDB Blog https://lobste.rs/s/giqysi #formalmethods
https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs

A Lean companion to “Analysis I” via @mseri https://lobste.rs/s/rzvbe9 #formalmethods #math
https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/

Systems Correctness Practices at Amazon Web Services https://lobste.rs/s/giokgl #formalmethods #testing
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/

The Coming AI Revolution in Distributed Systems https://lobste.rs/s/omtuek #formalmethods #vibecoding
https://zfhuang99.github.io/github%20copilot/formal%20verification/tla+/2025/05/24/ai-revolution-in-distributed-systems.html

What Works (and Doesn't) Selling Formal Methods https://lobste.rs/s/suuuaw #formalmethods
https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods

A Python frozenset interpretation of Dependent Type Theory

https://www.philipzucker.com/frozenset_dtt/

Discussions: https://discu.eu/q/https://www.philipzucker.com/frozenset_dtt/

The value of model checking in distributed protocols design https://lobste.rs/s/aeslga #distributed #formalmethods
https://protocols-made-fun.com/modelchecking/2025/04/08/value.html

A Python frozenset interpretation of Dependent Type Theory by @sandmouth https://lobste.rs/s/aohy4i #formalmethods #plt
https://www.philipzucker.com/frozenset_dtt/

New Life Hack: Using LLMs to Generate Constraint Solver Programs for Personal Logistics Tasks https://lobste.rs/s/wnrum7 #formalmethods #vibecoding
https://emschwartz.me/new-life-hack-using-llms-to-generate-constraint-solver-programs-for-personal-logistics-tasks/

A leap year check in three instructions https://lobste.rs/s/ybjgex #c #compilers #formalmethods
https://hueffner.de/falk/blog/a-leap-year-check-in-three-instructions.html