hmmm, if Cloudflare's Orange has been modeled in TLA+ for formal verification, has Signal been?

#signal #signalmessenger #cryptography #formalverification #TLAplus

@d10c4n3

Yes, this is another issue with the current #LLM architecture: they can't learn or improve. It's one big monolith - not composed of smaller parts (that could individually be improved or composed with each other).

There _are_ AI architectures that are _actually reliable_...

https://floss.social/@janriemer/114454349034565839

...but our industry has decided to hyperfocus on bullshit machines.

@larsmb

#ArtificialIntelligence #FormalVerification

Cryspen is excited to announce it has been awarded a grant from the Ethereum Foundation to extend our hax verification toolchain with support for the Lean prover. Watch this space for more on this soon!

#FormalVerification #Lean #Rust

Writing a Verified Postfix Expression Calculator (in Ada+SPARK)

https://pyjarrett.github.io/2025/06/10/postfix-calculator.html

#Ada #SPARK #formalVerification #Forth

Owi

https://github.com/OCamlPro/owi

Symbolic execution for #Wasm, #C, C++, #Rust and #Zig

"#Owi is an open-source framework for advanced #WebAssembly analysis and manipulation, with a focus on practical symbolic execution and robust tooling. It is designed for researchers, engineers, programming language enthusiasts and practitioners requiring precise, flexible, and extensible support program reasoning."

#FormalVerification #SoftwareTesting #Testing #SoftwareEngineering #RustLang #ZigLang

this is the bizness THE BIZNESS!! :cereal_killer:

The NVIDIA SPARK Process (GFDL v1.3) describing a software process using Ada/SPARK to meet ISO 26262.
https://nvidia.github.io/spark-process/

#Ada #SPARK #formalVerification

@sabik @dequbed @eniko @pixel

Totally agree! Unit tests and usage of #LLMs in that area are a bad combo (both for implementation and tests).

However, I'd like to give you some "food for thought":
What if the LLM was generating code against a (human written) #proof?

See this blog post, where they've written a proof with #Kani, a model checker in #Rust and let the #LLM generate the implementation until the proof passes:

https://model-checking.github.io/kani-verifier-blog/2023/05/01/writing-code-with-chatgpt-improve-it-with-kani.html

#FormalVerification #RustLang

"Fields 𝗠𝗲𝗱𝗮𝗹𝗶𝘀𝘁 𝗧𝗲𝗿𝗲𝗻𝗰𝗲 𝗧𝗮𝗼 𝗵𝗮𝘀 𝗮𝗻𝗻𝗼𝘂𝗻𝗰𝗲𝗱 𝗮𝗻 𝗲𝘅𝗰𝗶𝘁𝗶𝗻𝗴 𝗻𝗲𝘄 𝗽𝗿𝗼𝗷𝗲𝗰𝘁 𝗯𝗿𝗶𝗱𝗴𝗶𝗻𝗴 #FormalVerification and #MathematicsEducation: A #LeanLang companion to his foundational textbook 𝘈𝘯𝘢𝘭𝘺𝘴𝘪𝘴 𝘐."
https://bit.ly/4dNxX1d

People of ACM - Derek Dreyer

https://www.acm.org/articles/people-of-acm/2025/derek-dreyer

"Derek Dreyer is a Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) [...]. His [...] interests include type systems, semantics of programming languages, verification of concurrent programs, and interactive theorem proving. [...] His goal is “to produce rigorous formal foundations for establishing the safety and reliability of software systems.”"

#FormalVerification #Rust #RustLang #SoftwareEngineering

HACL*, a formally verified cryptographic library written in F*

https://github.com/hacl-star/hacl-star

#FStar #FStarLang #Cryptography #FormalVerification

Flux:

https://flux-rs.github.io/flux/

Flux is a refinement type checker for #Rust that lets you specify a range of correctness properties and have them be verified at compile time.

Crazy! :awesome:

#FormalVerification #RustLang

(❁´◡`❁)

#Rust pattern types RFC:
https://gist.github.com/joboet/0cecbce925ee2ad1ee3e5520cec81e30

Pattern types are a form of refinement types, which allow some subset of #FormalVerification!

https://en.wikipedia.org/wiki/Refinement_type

Tracking Issue for #PatternTypes:
https://github.com/rust-lang/rust/issues/123646

Tracking Issue for generic pattern types OwO:
https://github.com/rust-lang/rust/issues/136574

Implement minimal, internal-only pattern types in the type system:
https://github.com/rust-lang/rust/pull/120131

I'm _really_ looking forward to how #RustLang will evolve in this area!👀

#ProgrammingLanguage

The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:

1️⃣ "Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean

Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.

➡️ Watch Leo's lecture here: https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai

2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College

Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.

➡️ Watch Kevin's lecture here: https://podcasts.ox.ac.uk/will-computers-prove-theorems

#LeanLang #LeanProver #FormalVerification #Mathematics #AI #TheoremProving #OxfordCS

The Lean FRO team met synchronously in Amsterdam last week for our annual team retreat, and to discuss upcoming work and our Year 3 roadmap! 🇳🇱✨

We had very productive discussions around Lean's future in mathematics, software and hardware verification, and AI for math. It was energizing to see our team's commitment to Lean's continued growth in each of these domains.

We're cooking up many exciting developments that will support both our mathematical community and our growing base of software verification users. Stay tuned for our full Y3 roadmap publication at the end of July!

#LeanLang #LeanProver #Lean4 #FormalVerification #Programming #Mathematics #TheoremProving

Wow, #FuzzTesting/ #PropertyTesting is actually harder than doing an automatic proof.😓

I didn't expect that!😮

#SoftwareEngineering #Unexpected #Testing #FormalVerification

The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):

https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/

#Z3 #SMT #FormalVerification #ModelChecking #Proof

F* (fstar) Interactive Tutorial:

https://fstar-lang.org/tutorial/

I'm only like 10% into the tutorial, but this language is CRAZY (fun)! :awesome: 😄

I try to learn the fundamentals of it, so I can use the backend of it in #Aeneas... so I can ultimately formally verify my #Rust crate (former attempts with #Creusot and #Kani failed for me).

Aeneas:
https://github.com/AeneasVerif/aeneas

See part two of toot for a toy example of proving function equivalence

1/2

#FormalVerification #FunctionalProgramming #RustLang

Huh, seems like I really have been living on the bleeding edge (of #FormalVerification):

https://github.com/creusot-rs/creusot/discussions/1477#discussioncomment-12991148

The verification in the prev toot is currently not possible in #Creusot due to missing specs for the `Hash` trait and HashMap more broadly. 😔

Oh well, seems like (at least currently!) I won't be able to fully verify the diffing algorithm of #CSVDiff.🥺

Options I have now are:
- Only verify parts of the algorithm (that don't depend on HashMap ops)
or
- Use fuzzing/property testing

Readings shared April 27, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/27-readings_shared_04-27-25 #AI #CategoryTheory #CommonLisp #Emacs #FormalVerification #LogicProgramming #Prolog

AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. https://openreview.net/pdf?id=5t9HFssPla #AI #FormalVerification