#formalmethods

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

Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents https://lobste.rs/s/puijfw #compsci #formalmethods #unix https://arxiv.org/abs/2609.04043

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/

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

HOL Light Tutorial https://lobste.rs/s/zqa5yz #formalmethods #ml https://hol-light.github.io/tutorial/HTML/tutorial.html

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

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

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

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

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

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

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

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

Lambda MicroEgg by @sandmouth@types.pl https://lobste.rs/s/o6vyfj #formalmethods #plt https://www.philipzucker.com/lambda_miller_egg/

Semantics for 2D Rasterization https://lobste.rs/s/r84vto #formalmethods #graphics https://arxiv.org/abs/2603.23696

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

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/

Domain-specific hyperspecialization (for SAT) https://lobste.rs/s/cccby7 #formalmethods #vibecoding https://c.mov/lymphosat/

Formal methods with Hillel Wayne https://lobste.rs/s/gwdnwp #formalmethods #practices #testing https://newsletter.pragmaticengineer.com/p/formal-methods-with-hillel-wayne