Lmst

Isolation & Permissiveness of Distributed Transactions in MongoDB https://lobste.rs/s/6laiec #databases #distributed #formalmethods
https://www.mongodb.com/company/blog/engineering/formal-methods-beyond-correctness-isolation-permissiveness-distributed-transactions

The Intent Envelope: Proofs for Completeness, Not Just Soundness https://lobste.rs/s/cycn1o #ai #formalmethods
https://midspiral.com/blog/intent-envelope-proofs-for-completeness-not-just-soundness/

One-off Verified Transpilation with Claude https://lobste.rs/s/j4qtm1 #formalmethods #vibecoding
https://will62794.github.io/verification/llms/compilation/2026/01/20/bespoke-compilation.html

CSLib: A Focused Effort on Formalizing Computer Science in Lean https://lobste.rs/s/kv9qov #compsci #formalmethods #math
https://www.cslib.io/

Creusot 0.9.0: Launching the Creusot Devlog https://lobste.rs/s/igcrnj #formalmethods #rust
https://creusot-rs.github.io/devlog/2026-01-19/

#MULCIA: Post-doc position at Inria Rennes on AI and formal methods. https://is.gd/OKXP8D #PostDoc #CompSci #AI #FormalMethods

"Beware of bugs in the above code; I have only proved it correct, not tried it." – Donald Knuth

Pitting formal verification against an LLM to generate proofs seems like an obvious use case for AI, but theorem provers are not inherently robust against adversarial agents. Reward hacking theorem provers is possible.

They may use non-constructive axioms to trivialize a proof, or use backdoors like trusted tags and metaprogramming to redefine logical operations, effectively "proving" false statements.

https://www.lesswrong.com/posts/rhAPh3YzhPoBNpgHg/lies-damned-lies-and-proofs-formal-methods-are-not-slopless

#formalMethods

Test, don't (just) verify https://lobste.rs/s/radysr #formalmethods #testing
https://alperenkeles.com/posts/test-dont-verify/

Quint Visualizer: a GraphViz-like visualizer for Quint traces https://lobste.rs/s/09tygd #show #distributed #formalmethods
https://quint-visualizer.noghartt.dev/

Writing Anteforth, a Forth-like in SPARK https://lobste.rs/s/8hjgvt #concatenative #formalmethods
https://pyjarrett.github.io/2026/01/13/anteforth.html

Verifying State & Reconciliation in Collaborative Web Apps https://lobste.rs/s/yxg4xt #ai #formalmethods
https://midspiral.com/blog/verifying-state-reconciliation-in-collaborative-web-apps/

https://www.yodaiken.com/2022/05/07/process-algebra-and-automata-theory/
#computerscience #verification #formalmethods #processalgebra

New release! It's also a better one, not just new. We improved some features and squashed some bugs. And improved documentation based on used feedback. Good stuff, even if we say so ourselves.

https://www.provengo.ai/post/new-year-new-release

#FormalMethods #QAAutomation #DevTools #FMWinterIsOver