#formalmethods — Public Fediverse posts

🆕 A blueprint for formal verification of Apple corecrypto

Learn more about the formal verification methods used for ensuring the mathematical correctness of corecrypto's post-quantum ML-KEM and ML-DSA implementations.
We are also releasing our Isabelle libraries, ARM64 model, and Cryptol-to-Isabelle translator!

https://security.apple.com/blog/formal-verification-corecrypto/

#FormalMethods #PostQuantum #Security

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications https://lobste.rs/s/ukw5wf #formalmethods #testing #vibecoding
https://proofsandintuitions.net/2026/05/18/property-based-testing-specifications/

[New Blog Post] Reading Proof Objects and Completed Rewrite Systems from eprover into Knuckledragger https://www.philipzucker.com/proof_processing/ #python #logic #automatedtheoremproving #formalmethods

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

Next week I am going to Tokyo to give a presentation at the ABZ 2026 conference. Title: “Identifying Design Flaws in a Lock-Free Task Pool with TLA+”. It is an “application in industry” paper, I will upload it and the slides a bit later

We specified an algorithm with the simple goal of confirming its correctness, and instead found numerous issues without an obvious way to fix them (if it is even possible). Finding this early saved us huge amount of time and resources, and i think the result is quite a bit unusual

ABZ is my favorite conference, it is about state-based #formalmethods like Alloy, Event-B and #TLA+. The papers are always interesting, and each conference has a “case study” track, in which practitioners specify the given system using any state-based method they want and describe the results and their observations. This time the system is an autonomous planetary rover

Side note: my first trip abroad was back in 2014, and it was also to speak at ABZ :) I even met and spoke with Jean-Raymond Abrial!

https://abz-conf.org/site/2026/

What Happens to Software When Proof is Cheap? https://lobste.rs/s/r8epo9 #video #formalmethods #vibecoding
https://www.youtube.com/watch?v=oSHVPvM56sA

🚨 the @securedrop team at Freedom of Press Foundation is hiring 🚨

We're looking for a Cryptography Engineer to help us build out the new end-to-end encrypted version of #SecureDrop

✔️ fully remote (must be US based)
✔️ all FOSS
✔️ help secure whistleblowers and investigative journalists all around the world

More details in the job posting, happy to answer any questions

https://freedomofthepress.na.teamtailor.com/jobs/610227-cryptography-engineer

:boost_ok:

#GetFediHired #Rust #FormalMethods #Encryption #Cryptography #Whistleblowing #OpenSource

🚨 the @securedrop team at Freedom of Press Foundation is hiring 🚨

We're looking for a Cryptography Engineer to help us build out the new end-to-end encrypted version of #SecureDrop

✔️ fully remote (must be US based)
✔️ all FOSS
✔️ help secure whistleblowers and investigative journalists all around the world

More details in the job posting, happy to answer any questions

https://freedomofthepress.na.teamtailor.com/jobs/610227-cryptography-engineer

:boost_ok:

#GetFediHired #Rust #FormalMethods #Encryption #Cryptography #Whistleblowing #OpenSource

🚨 the @securedrop team at Freedom of Press Foundation is hiring 🚨

We're looking for a Cryptography Engineer to help us build out the new end-to-end encrypted version of #SecureDrop

✔️ fully remote (must be US based)
✔️ all FOSS
✔️ help secure whistleblowers and investigative journalists all around the world

More details in the job posting, happy to answer any questions

https://freedomofthepress.na.teamtailor.com/jobs/610227-cryptography-engineer

:boost_ok:

#GetFediHired #Rust #FormalMethods #Encryption #Cryptography #Whistleblowing #OpenSource

🚨 the @securedrop team at Freedom of Press Foundation is hiring 🚨

We're looking for a Cryptography Engineer to help us build out the new end-to-end encrypted version of #SecureDrop

✔️ fully remote (must be US based)
✔️ all FOSS
✔️ help secure whistleblowers and investigative journalists all around the world

More details in the job posting, happy to answer any questions

https://freedomofthepress.na.teamtailor.com/jobs/610227-cryptography-engineer

:boost_ok:

#GetFediHired #Rust #FormalMethods #Encryption #Cryptography #Whistleblowing #OpenSource

🚨 the @securedrop team at Freedom of Press Foundation is hiring 🚨

We're looking for a Cryptography Engineer to help us build out the new end-to-end encrypted version of #SecureDrop

✔️ fully remote (must be US based)
✔️ all FOSS
✔️ help secure whistleblowers and investigative journalists all around the world

More details in the job posting, happy to answer any questions

https://freedomofthepress.na.teamtailor.com/jobs/610227-cryptography-engineer

:boost_ok:

#GetFediHired #Rust #FormalMethods #Encryption #Cryptography #Whistleblowing #OpenSource

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

Generality brings further utility. Based on HasFresh, CSLib's free_union tactic will automatically look at your context for you and try to collect all current values into a finite set. You can then use HasFresh's API to get a fresh value that is different from all those in your context.
Just like on pen and paper: pick a fresh x!

Check out HasFresh at https://api.cslib.io/docs/Cslib/Foundations/Data/HasFresh.html

#FormalMethods #FORM

3/3

Generality brings further utility. Based on HasFresh, CSLib's free_union tactic will automatically look at your context for you and try to collect all current values into a finite set. You can then use HasFresh's API to get a fresh value that is different from all those in your context.
Just like on pen and paper: pick a fresh x!

Check out HasFresh at https://api.cslib.io/docs/Cslib/Foundations/Data/HasFresh.html

#FormalMethods #FORM

3/3

Proving Liveness with TLA

https://roscidus.com/blog/blog/2026/01/01/tla-liveness/

#HackerNews #Proving #Liveness #TLA #FormalMethods #DistributedSystems

Here is a very nice experience report of conformance checking between #TLA+ specs and implementation, covering both test-case generation and trace checking: https://www.mongodb.com/company/blog/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs

There are a lot of links to other reports and papers, I recommend to check them out too.

#formalmethods #formalverification

Systems Correctness Practices at Amazon Web Services. Leveraging formal and semi-formal methods.
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/

#TLA #FormalMethods #softwareEngineering

Microsoft's hyperscale AI infrastructure: a formal specification problem. How to guarantee performance, energy sustainability & regulatory compliance at 1.35 GW scale while integrating Anthropic Claude + NVIDIA partnerships. Analysis: https://post.kapualabs.com/4jv63f28 #AI #Microsoft #CloudInfrastructure #FormalMethods $MSFT

The Final Form of Software Development https://lobste.rs/s/gcljqi #cryptography #formalmethods #vibecoding #virtualization
https://blog.zksecurity.xyz/posts/end-coding/

Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

https://arxiv.org/abs/2512.02080

#HackerNews #Designing #Predictable #LLM-Verifier #Systems #for #Formal #Method #Guarantee #LLMVerifier #FormalMethods #AIResearch #Predictability #arXiv

Readings shared April 29, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/30-readings_shared_04-29-26 #AI4Math #Agda #Emacs #FormalMethods #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math

My Verification of Autonomous Systems book is finally out!

In addition to contributed chapters on theoretical and practical aspects of verifying autonomy*, the editors contributed an introduction on stakeholder perspectives and a chapter on the specific challenges autonomy introduces to verification.

Each chapter is cross-referenced to e challenges it addresses in a handy table to help readers find the information most useful to them.

I'm really proud of all our authors! So many thanks to everyone who contributed^, especially my co-editors, Mae Seto, Don Sofge, and John Sustersic!

E-book now available for download and hard copy coming soon!

* This book is about verifying autonomous embodied robots, not LLMs or AI models.

^ No AI was used in the generation of this book's content.

Link: https://link.springer.com/book/10.1007/978-3-031-88546-4

#Robotics #AutonomousSystems #Verification #VerificationOfAutonomy #Robots #AutonomousRobots #CyberPhysicalSystems #RobotTesting #FormalMethods #Modeling #Simulation

Verifying the #Rust Standard Library - Carolyn Zech, Amazon Web Services

https://invidious.nerdvpn.de/watch?v=8_lzVNs1uPk
(or YT: https://www.youtube.com/watch?v=8_lzVNs1uPk)

Carolyn is also a maintainer of #Kani, the Rust model checker.
She has been so supportive and kind during my struggles with HashMaps and Kani 🥺

https://github.com/model-checking/kani/issues/3965

Give her a follow:
https://github.com/carolynzech

#FormalVerification #FormalMethods #RustLang #Testing #SoftwareEngineering

Catching up on some of the really great talks from the Zurich DVClub on RISC-V Verification
https://alpinumconsulting.com/dv-club-zurich-riscv-verification/
#DV #SiliconEngineering #RISCV #FormalMethods #FV

Next talk is by prof. Rubin's PhD advisor: prof. Marsha Chechik. She's talking about academic research (next talk will be about industry research).

#WomenInTech #WomenInComputing #WomenInSTEM #FormalMethods #ArtificialIntelligence #SoftwareEngineering #ESEC #FSE

quint-connect: A model-based testing framework for Quint + Rust https://lobste.rs/s/ggptr5 #formalmethods #rust
https://github.com/informalsystems/quint-connect

Illegal vs Unwanted States https://lobste.rs/s/szrxqe #formalmethods
https://buttondown.com/hillelwayne/archive/illegal-vs-unwanted-states/

Illegal vs Unwanted States

https://fed.brid.gy/r/https://buttondown.com/hillelwayne/archive/illegal-vs-unwanted-states/

"Why not just use Lean?" https://lobste.rs/s/d27llp #formalmethods
https://lawrencecpaulson.github.io/2026/04/23/Why_not_Lean.html

"Why not just use Lean?"

https://fed.brid.gy/r/https://lawrencecpaulson.github.io/2026/04/23/Why_not_Lean.html

What works and doesn't selling formal methods in industry. ~ Mike Dodds. https://youtu.be/Z2bTpsO4fcc #FormalMethods

LemmaScript: A Verification Toolchain for TypeScript via Dafny https://lobste.rs/s/4tuujf #formalmethods
https://midspiral.com/blog/lemmascript-a-verification-toolchain-for-typescript/

Meet 'n' Prove is the opportunity to find out about research and teaching on formal methods.
Find out more about our research and about opportunities for final theses or student jobs!
6 research groups - all focussing on formal methods - will present their work:

Please let us know if you plan to attend the event: https://s.kit.edu/mnp
Spontaneous participation is still possible!
#formalMethods #kitinformatik

Signal Shot: a project to verify the Signal protocol and its Rust implementation using Lean https://lobste.rs/s/jnl6e7 #cryptography #formalmethods #security #vibecoding
https://leodemoura.github.io/blog/2026-4-20-signal-shot-the-platform-is-ready/

Signal Shot: a project to verify the Signal protocol and its Rust implementation using Lean

https://fed.brid.gy/r/https://leodemoura.github.io/blog/2026-4-20-signal-shot-the-platform-is-ready/

<hmmm-on-a-tangent/>

What if such nasty things also bring about an increased demand for program verification using formal methods?

Yes, it is difficult, but even partial solutions are helpful and way, way better than nothing.

By the way, I ought to look for any surveys on the use of assertions (the little cousins of program verification) in published program sources.

One old textbook I found well worth reading was the one about program specification and software development by Liskov and Guttag.
The first edition, using the CLU programming language.

#ComputerProgramming
#IHaveADream
#FormalMethods
#ProgramVerification
#SoftwareEngineering

@screwlisp

Building an Unverified Compiler with Agents https://lobste.rs/s/fkxdc8 #formalmethods #plt #vibecoding
https://www.basis.ai/blog/verified-compiler/

A sufficiently comprehensive spec is not (necessarily) code https://lobste.rs/s/u1fem9 #formalmethods #vibecoding
https://buttondown.com/hillelwayne/archive/a-sufficiently-comprehensive-spec-is-not/

🚀 CSLib is Growing – Follow Its Journey!

The #Lean Computer Science Library (#CSLib) – a global effort to build reusable infrastructure for formal methods in AI-ready computer programming and research – is gaining momentum (> 100 forks, > 400 PRs, and nearly 500 stars on GitHub).

If you’re curious about its progress, the contributions we seek, or the open challenges we’re discussing, watch this space. I’ll start sharing updates about these topics soon.

#FormalMethods @acp

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

Lean proved this program was correct; then I found a bug

https://fed.brid.gy/r/https://kirancodes.me/posts/log-who-watches-the-watchers.html

How NASA Built Artemis II’s Fault-Tolerant Computer https://lobste.rs/s/nomyva #distributed #formalmethods #hardware #testing
https://cacm.acm.org/news/how-nasa-built-artemis-iis-fault-tolerant-computer/

Giving LLMs a Formal Reasoning Engine for Code Analysis https://lobste.rs/s/fu9wcm #formalmethods #vibecoding
https://yogthos.net/posts/2026-04-08-neurosymbolic-mcp.html