The Final Form of Software Development https://lobste.rs/s/gcljqi #cryptography #formalmethods #vibecoding #virtualization
https://blog.zksecurity.xyz/posts/end-coding/
formalmethods
quint-connect: A model-based testing framework for Quint + Rust https://lobste.rs/s/ggptr5 #formalmethods #rust
https://github.com/informalsystems/quint-connect
Lean proved this program was correct; then I found a bug https://lobste.rs/s/wwr6zu #formalmethods #plt #security
https://kirancodes.me/posts/log-who-watches-the-watchers.html
The fall of the theorem economy https://lobste.rs/s/fid0x2 #formalmethods #math #vibecoding
https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy
Who Builds a House Without Drawing Blueprints? (2015) https://lobste.rs/s/omounu #formalmethods
https://cacm.acm.org/opinion/who-builds-a-house-without-drawing-blueprints/
Foundational Verification of Running-Time Bounds for Interactive Programs https://lobste.rs/s/r1ezk0 #pdf #formalmethods #performance
https://adam.chlipala.net/papers/MetricsCPP26/MetricsCPP26.pdf
Proving the Fundamental Theorem of Arithmetic in Agda via @abnv https://lobste.rs/s/s61wns #formalmethods #math
https://byorgey.github.io/blog/posts/2026/06/26/FTA.lagda.html
You Don’t Know Jack About Formal Verification https://lobste.rs/s/ugm5fn #formalmethods
https://queue.acm.org/detail.cfm?id=3819084
EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation https://lobste.rs/s/efnxre #formalmethods #osdev #security #virtualization
https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation
Formal methods and the future of programming https://lobste.rs/s/mpotqq #formalmethods
https://blog.janestreet.com/formal-methods-at-jane-street-index
Palomar – a registry of Lean verified mathematics https://lobste.rs/s/rjxezi #formalmethods #math
https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/
Xavier Leroy on programming, languages and formal verification via @xvw https://lobste.rs/s/oviysl #video #formalmethods #ml
https://www.youtube.com/watch?v=9Cswiqrq6So
Extending MVCC to be serializable, in TLA+ (2024) https://lobste.rs/s/yodbwx #databases #formalmethods
https://surfingcomplexity.blog/2024/11/03/extending-mvcc-to-be-serializable-in-tla/
Fast DEFLATE compression in Lean https://lobste.rs/s/1o4ba2 #formalmethods #performance #vibecoding
https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/
Why Rocq is better than Lean for program verification https://lobste.rs/s/vnh6b2 #compilers #formalmethods #ml #plt
https://joomy.korkutblech.com/posts/2026-07-28-why-rocq-is-better.html
Formal methods with Hillel Wayne https://lobste.rs/s/gwdnwp #formalmethods #practices #testing
https://newsletter.pragmaticengineer.com/p/formal-methods-with-hillel-wayne
An Anecdote Against Slop Artifacts https://lobste.rs/s/7tjseu #formalmethods #vibecoding
https://www.markusde.ca/pages/noslop.html
Improving system safety with Temporal Logic of Actions (TLA+) https://lobste.rs/s/ues1ak #formalmethods #vibecoding
https://depot.dev/blog/tla-verification
How to Find Bugs in Systems That Don't Exist https://lobste.rs/s/izdtd6 #video #formalmethods #practices
https://www.youtube.com/watch?v=zSZkLyD9ILI
#lispyGopherClimate very haphazard Sunday-morning-in-Europe #peertube #live weekly #technology #podcast
@alexshendi #lisp and possibly @jhlagado we are going to meet up in #lambdaMOO and on the livestream and talk about lisp and retrocomputing and modern computing.
https://toobnix.org/w/g2AftRUaBvEVGfJYMY1MHr
John Hardy's git feat. vintage game tape WAV https://github.com/jhlagado
and @ramin_hal9001 ! And @rat in-MOO!
Computer origins, #xlisp, #z80, #formalMethods ..! #bookstodon #neuromancer #godelEscherBAch
Edited 11d ago
A preview of the future Intel Architecture documentation https://lobste.rs/s/cywxla #formalmethods #hardware
https://intel.github.io/SDM/announcement/2026/08/20/announce-preview.html
My EuroSys 2026 paper is obsolete https://lobste.rs/s/stecbz #formalmethods #vibecoding
https://claudiacauli.com/2026/03/08/my-eurosys-2026-paper-is-obsolete/
WebCorC: Tool support for Correctness-by-Construction developed at Karlsruhe Institute of Technology https://lobste.rs/s/zvpelp #formalmethods #plt
https://github.com/KIT-TVA/WebCorC