HACL*, a formally verified cryptographic library written in F*
Recent searches
Search options
#formalverification
4 posts2 participants0 posts today
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! 
flux-rs.github.ioIntroduction - Flux Documentation
(❁´◡`❁)
#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!
GistPattern types RFCPattern types RFC. GitHub Gist: instantly share code, notes, and snippets.
The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:
"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
"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
podcasts.ox.ac.ukFormalizing the Future: Lean’s Impact on Mathematics, Programming, and AIHow can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate.
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!
Wow, #FuzzTesting/ #PropertyTesting is actually harder than doing an automatic proof.
I didn't expect that!
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/
Microsoft Research · Model-based approach behind Z3 theorem prover’s efficiency, powerIn 10-plus years, the Z3 theorem prover has surpassed the use cases that motivated its design in exciting ways. Researchers Nikolaj Bjørner and Leonardo de Moura explain how a model-based approach has contributed to the SMT solver’s success.
F* (fstar) Interactive Tutorial:
https://fstar-lang.org/tutorial/
I'm only like 10% into the tutorial, but this language is CRAZY (fun)! 
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
fstar-lang.orgF* Tutorial
Continued thread
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
Vestigium · Readings shared April 27, 2025The readings shared in Bluesky on 27 April 2025 are
Bitcoinolog: Reason about Bitcoin addresses with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
Working with Common Lisp pathnames. ~ Nicolas M
AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. https://openreview.net/pdf?id=5t9HFssPla #AI #FormalVerification
Hm...I'm running into a timeout with #Creusot when trying to verify a simple `add` operation on a HashMap newtype 
https://github.com/creusot-rs/creusot/discussions/1477
Does anyone have any idea what's going on here?
Disclaimer: I'm totally new to creusot and #FormalVerification, so please be gentle with me.
Boosts very much appreciated. 
Thank you! 
Place Capability Graphs: A General-Purpose Model of #Rust’s
Ownership and Borrowing Guarantees (April 2025)
https://arxiv.org/pdf/2503.21691
"We present a novel model of Rust’s type-checking [...], which lifts [...] limitations [of current verification tools], and which can be directly calculated from the #RustLang compiler’s own programmatic representations and analyses. We demonstrate that our model supports over 98% of Rust functions in the most popular public crates...
1/2
creuSAT - A formally verified #SAT solver written in #Rust and verified with #Creusot.
https://github.com/sarsko/CreuSAT
Mindblowing! 
Co-Developing Programs and Their Proof of Correctness - the SPARK Programming Language and Analyzer
https://cacm.acm.org/research/co-developing-programs-and-their-proof-of-correctness/
Communications of the ACM · Co-Developing Programs and Their Proof of Correctness
Continued thread
Re: Help us create a vision for Rust's future 
In the mid- to long-term I can see #Rust focus more and more on facilitating #FormalVerification - it perfectly aligns with #RustLang's vision of enabling everyone to build _reliable_ and efficient software.
First step is probably to have a common contract language, which might enable interoperability of different verification tools.
(Disclaimer: I'm a total newbie in the field of formal verification, but I find it absolutely fascinating!)
Iris Project | A Higher-Order Concurrent Separation Logic Framework,
implemented and verified in the Rocq Prover
iris-project.orgIris Project
New blog post! 
Control flow analysis with Hax. In this post we show how to ensure control flow properties such as "function A is always called before function B" in Rust. Super relevant for security! 
Formal Verification for Machine Learning Models Using Lean 4