Stories tagged as formalmethods Formal methods

Most often also tagged with plt security c math testing compsci compilers distributed

  1. 25
    Formal methods and the future of programming blog.janestreet.com
    via nextos
    caches
    1 comment
  2. 20
    EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation amazon.science
    via amw-zero
    caches
    9 comments
  3. 16
    hax: A Rust verification tool github.com/cryspen
    via jado
    caches
    no comments
  4. 8
    Announcing Isabelle support for SAW galois.com
    via olliej
    caches
    2 comments
  5. 25
    A blueprint for formal verification of Apple corecrypto security.apple.com
    via typesanitizer
    caches
    2 comments
  6. 5
    Who Builds a House Without Drawing Blueprints? (2015) cacm.acm.org
    via typesanitizer
    caches
    2 comments
  7. 1
    A Revolution in Mathematics? What Really Happened a Century Ago and Why It Matters Today (2012) ☶ ams.org
    via safinaskar
    caches
    3 comments
  8. 7
    On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications proofsandintuitions.net
    via typesanitizer
    caches
    no comments
  9. 35
    How we used Quint to find over 10 bugs in SQLite while hardening Turso turso.tech
    via typesanitizer
    caches
    6 comments
  10. 2
    Using algebra and LLMs to verify a flight-plan bug fix in Lean jameshaydon.github.io
    authored by jameshh
    caches
    no comments
  11. 3
    Requirements analysis: catching requirement bugs before they become code kiro.dev
    via inactive-user
    caches
    1 comment
  12. 2
    What Happens to Software When Proof is Cheap? ☶ youtube.com
    via joomy
    caches
    no comments
  13. 11
    The fall of the theorem economy davidbessis.substack.com
    via safinaskar
    caches
    no comments
  14. 2
    quint-connect: A model-based testing framework for Quint + Rust github.com/informalsystems
    via hwayne
    caches
    no comments
  15. 3
    The Final Form of Software Development blog.zksecurity.xyz
    via mimoo
    caches
    1 comment
  16. 34
    Illegal vs Unwanted States buttondown.com/hillelwayne
    via ajdecon
    caches
    8 comments
  17. 51
    "Why not just use Lean?" lawrencecpaulson.github.io
    via priime
    caches
    9 comments
  18. 10
    LemmaScript: A Verification Toolchain for TypeScript via Dafny midspiral.com
    authored by namin
    caches
    no comments
  19. 19
    Signal Shot: a project to verify the Signal protocol and its Rust implementation using Lean leodemoura.github.io
    via sanxiyn
    caches
    4 comments
  20. 12
    Creusot 0.11.0: VerifyThis winner devlog.creusot.rs
    authored by lyxia
    caches
    no comments
  21. 3
    Building an Unverified Compiler with Agents basis.ai
    via kirancodes
    caches
    no comments
  22. 9
    A sufficiently comprehensive spec is not (necessarily) code buttondown.com/hillelwayne
    via amw-zero
    caches
    1 comment
  23. 75
    Lean proved this program was correct; then I found a bug kirancodes.me
    authored by kirancodes
    caches
    25 comments
  24. 22
    How NASA Built Artemis II’s Fault-Tolerant Computer cacm.acm.org
    via owi
    caches
    6 comments
  25. 16
    Giving LLMs a Formal Reasoning Engine for Code Analysis yogthos.net
    authored by Yogthos
    caches
    17 comments

Tip: read stories across multiple tags with /t/tag1,tag2