Mastodawn

A blueprint for formal verification of Apple corecrypto

https://fed.brid.gy/r/https://security.apple.com/blog/formal-verification-corecrypto/

Announcing Isabelle support for SAW https://lobste.rs/s/xha7ff #cryptography #formalmethods
https://www.galois.com/articles/announcing-isabelle-support-for-saw

Announcing Isabelle support for SAW

1 comment

Lobsters

Lobsters 1d ago

A blueprint for formal verification of Apple corecrypto https://lobste.rs/s/7crjja #cryptography #formalmethods
https://security.apple.com/blog/formal-verification-corecrypto/

A blueprint for formal verification of Apple corecrypto

0 comments

Lobsters

Frédéric Jacobs 2d ago

🆕 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

Lobsters 3d ago

Who Builds a House Without Drawing Blueprints? (2015)

https://cacm.acm.org/opinion/who-builds-a-house-without-drawing-blueprints/

#SoftwareEngineering #Architecture #FormalMethods

Who Builds a House Without Drawing Blueprints?

Communications of the ACM

Lobsters 3d ago

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/

Who Builds a House Without Drawing Blueprints? (2015)

0 comments

Lobsters

Lobsters [Unofficial]5d ago

How we used Quint to find over 10 bugs in SQLite while hardening Turso

https://fed.brid.gy/r/https://turso.tech/blog/how-we-used-quint-to-find-over-10-bugs-in-sqlite

Lobsters 5d ago

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications

https://proofsandintuitions.net/2026/05/18/property-based-testing-specifications/

#Testing #SoftwareEngineering #FormalMethods

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications

In this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which helped to detect underspecification in 10% of the specs in state-of-the-art benchmarks for verified code generation.

Proofs and Intuitions

Lobsters 5d ago

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/

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications

0 comments

Lobsters

sayzard 5d ago

We used Quint to find over 10 bugs in SQLite while hardening Turso

Turso 커뮤니티 멤버가 Quint라는 형식적 검증 도구를 활용해 SQLite C API를 모델링하고 테스트하면서 SQLite에서 10개 이상의 버그를 발견했다. Quint는 TLA+ 기반으로 상태 추적을 생성해 실제 SQLite 동작과 비교하며, 기존 테스트로는 발견하기 어려웠던 결함을 찾아냈다. 이 과정에서 sqlite3_deserialize() 함수의 크래시 문제 등 중요한 버그들이 수정되었으며, Turso와 SQLite 모두 품질 향상에 기여했다. 형식적 방법론의 실무 적용 가능성을 보여준 사례다.

https://turso.tech/blog/how-we-used-quint-to-find-over-10-bugs-in-sqlite

#sqlite #formalmethods #quint #testing #opensource

How we used Quint to find over 10 bugs in SQLite while hardening Turso

Pavan Nambi used Quint to model the SQLite C API, generate traces, and run them against SQLite. The exercise hardened Turso and surfaced over 10 bugs in SQLite itself.