formalmethods

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/

Ship Your Interpreter https://lobste.rs/s/rtd5gq #formalmethods #vibecoding
https://www.basis.ai/blog/ship-your-interpreters/

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

Can we have reachability properties in TLA⁺? by @ahelwer https://lobste.rs/s/8pjbtj #formalmethods
https://ahelwer.ca/post/2026-09-26-reachability/

Ghidra + CBMC = Assembly Model Checker https://lobste.rs/s/br0hd7 #formalmethods
https://www.philipzucker.com/asmc_cpp/

I built the RealWorld app in Lean 4 https://lobste.rs/s/xctcdf #formalmethods #vibecoding
https://leangineer.com/blog/realworld-in-lean/

Foundational Cryptography in SPARK https://lobste.rs/s/sd75mw #cryptography #formalmethods
https://www.adacore.com/blog/foundational-cryptography-in-spark

DogWood: Monitoring Policies using First Order Temporal Logic via @agnishom https://lobste.rs/s/69mmo0 #formalmethods #programming
https://aws.amazon.com/blogs/opensource/introducing-dogwood-runtime-verification-for-ai-agents/

What TLA+ can and can't check https://lobste.rs/s/3ufaju #formalmethods
https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/

Full-stack verification is the new trend https://lobste.rs/s/lerlry #ai #formalmethods
https://wiki.alcidesfonseca.com/blog/full-stack-verification-is-the-new-trend/

Refinement E-Graphs by @sandmouth https://lobste.rs/s/9bufek #compilers #formalmethods
https://www.philipzucker.com/refinement_egraph/

How we continuously validate formal specifications in production https://lobste.rs/s/gzdimd #formalmethods #testing
https://www.datadoghq.com/blog/engineering/continuous-formal-spec-validation/

Impossibility Proof for Instant 8-tuple Piston Extenders https://lobste.rs/s/r07fdn #video #formalmethods #games #math #reversing
https://www.youtube.com/watch?v=I-MMyRzmqFI

How to Believe a Machine-Checked Proof (1997) https://lobste.rs/s/8nfjfc #pdf #formalmethods #math
https://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf

Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs https://lobste.rs/s/axmhji #pdf #formalmethods #math #reversing #vibecoding
https://arxiv.org/abs/2610.08144

Creusot 0.14.0 release - Contracts for Rust, formally proved https://lobste.rs/s/6tbd2o #formalmethods #rust
https://devlog.creusot.rs/v0-14-0/