Mathstodon

Jan :rust: :ferris:Wow, <a href="https://floss.social/tags/FuzzTesting" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FuzzTesting</a>/ <a href="https://floss.social/tags/PropertyTesting" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PropertyTesting</a> is actually harder than doing an automatic proof.😓 I didn't expect that!😮 <a href="https://floss.social/tags/SoftwareEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SoftwareEngineering</a> <a href="https://floss.social/tags/Unexpected" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Unexpected</a> <a href="https://floss.social/tags/Testing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Testing</a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a>

Jan :rust: :ferris:The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):<a href="https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/</a><a href="https://floss.social/tags/Z3" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Z3</a> <a href="https://floss.social/tags/SMT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SMT</a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ModelChecking</a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Proof</a>

Jan :rust: :ferris:F* (fstar) Interactive Tutorial:<a href="https://fstar-lang.org/tutorial/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://fstar-lang.org/tutorial/</a>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 <a href="https://floss.social/tags/Aeneas" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Aeneas</a>... so I can ultimately formally verify my <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> crate (former attempts with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> and <a href="https://floss.social/tags/Kani" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Kani</a> failed for me).Aeneas: <a href="https://github.com/AeneasVerif/aeneas" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/AeneasVerif/aeneas</a>See part two of toot for a toy example of proving function equivalence1/2<a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a>

Jan :rust: :ferris:Huh, seems like I really have been living on the bleeding edge (of <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a>):<a href="https://github.com/creusot-rs/creusot/discussions/1477#discussioncomment-12991148" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/creusot-rs/creusot/discussions/1477#discussioncomment-12991148</a>The verification in the prev toot is currently not possible in <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> 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 <a href="https://floss.social/tags/CSVDiff" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CSVDiff</a>.🥺 Options I have now are: - Only verify parts of the algorithm (that don't depend on HashMap ops) or - Use fuzzing/property testing

José A. AlonsoReadings shared April 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/27-readings_shared_04-27-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/04/27-readings_shared_04-27-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="tag">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#CommonLisp</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="tag">#Emacs</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#Prolog</a>

LavX NewsRevolutionizing Testing: The Rise of Code-Free Validation in Software DevelopmentIn a groundbreaking shift for software development, the concept of testing without executing code is gaining traction. This innovative approach not only streamlines the development process but also en...<a href="https://news.lavx.hu/article/revolutionizing-testing-the-rise-of-code-free-validation-in-software-development" rel="nofollow noopener noreferrer" target="_blank">https://news.lavx.hu/article/revolutionizing-testing-the-rise-of-code-free-validation-in-software-development</a><a href="https://mastodon.cloud/tags/news" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#news</a> <a href="https://mastodon.cloud/tags/tech" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#tech</a> <a href="https://mastodon.cloud/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://mastodon.cloud/tags/StaticAnalysis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#StaticAnalysis</a> <a href="https://mastodon.cloud/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ModelChecking</a>

José A. AlonsoAI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. <a href="https://openreview.net/pdf?id=5t9HFssPla" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://openreview.net/pdf?id=5t9HFssPla</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a>

Jan :rust: :ferris:Hm...I'm running into a timeout with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a> when trying to verify a simple `add` operation on a HashMap newtype 🤔 <a href="https://github.com/creusot-rs/creusot/discussions/1477" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/creusot-rs/creusot/discussions/1477</a>Does anyone have any idea what's going on here?Disclaimer: I'm totally new to creusot and <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a>, so please be gentle with me.😊 Boosts very much appreciated. :boost_love: Thank you! ❤️ <a href="https://floss.social/tags/IDontKnowWhatIamDoing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IDontKnowWhatIamDoing</a> <a href="https://floss.social/tags/Help" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Help</a> <a href="https://floss.social/tags/FediHelp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FediHelp</a> <a href="https://floss.social/tags/FollowerPower" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FollowerPower</a> <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Proof</a> <a href="https://floss.social/tags/Timeout" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Timeout</a>

Jan :rust: :ferris:Place Capability Graphs: A General-Purpose Model of <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a>’s Ownership and Borrowing Guarantees (April 2025)<a href="https://arxiv.org/pdf/2503.21691" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/pdf/2503.21691</a>"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 <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a> 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<a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a>

Jan :rust: :ferris:creuSAT - A formally verified <a href="https://floss.social/tags/SAT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SAT</a> solver written in <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> and verified with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Creusot</a>.<a href="https://github.com/sarsko/CreuSAT" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/sarsko/CreuSAT</a>Mindblowing! 🤯 <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a>

Jan :rust: :ferris:Co-Developing Programs and Their Proof of Correctness - the SPARK Programming Language and Analyzer<a href="https://cacm.acm.org/research/co-developing-programs-and-their-proof-of-correctness/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://cacm.acm.org/research/co-developing-programs-and-their-proof-of-correctness/</a><a href="https://floss.social/tags/SPARK" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SPARK</a> <a href="https://floss.social/tags/Ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Ada</a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/SoftwareDevelopment" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SoftwareDevelopment</a> <a href="https://floss.social/tags/Quality" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Quality</a>

Jan :rust: :ferris:Re: Help us create a vision for Rust's future 👆 In the mid- to long-term I can see <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> focus more and more on facilitating <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> - it perfectly aligns with <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RustLang</a>'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!)

Jan :rust: :ferris:Iris Project | A Higher-Order Concurrent Separation Logic Framework, implemented and verified in the Rocq Prover<a href="https://iris-project.org/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://iris-project.org/</a><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/Iris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Iris</a> <a href="https://floss.social/tags/ConcurrentSeparationLogic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ConcurrentSeparationLogic</a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Proof</a>

CryspenNew 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! 🔒<a href="https://cryspen.com/post/control-flow-analysis/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://cryspen.com/post/control-flow-analysis/</a><a href="https://ioc.exchange/tags/rustlang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#rustlang</a> <a href="https://ioc.exchange/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalverification</a> <a href="https://ioc.exchange/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#security</a>

Hacker NewsFormal Verification for Machine Learning Models Using Lean 4<a href="https://github.com/fraware/leanverifier" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/fraware/leanverifier</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://mastodon.social/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineLearning</a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lean4</a> <a href="https://mastodon.social/tags/AIResearch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AIResearch</a> <a href="https://mastodon.social/tags/TechInnovation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TechInnovation</a>

José A. AlonsoReadings shared March 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/19-readings_shared_03-19-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/03/19-readings_shared_03-19-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="tag">#CompSci</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/Programaci%C3%B3nFuncional" class="mention hashtag" rel="tag">#ProgramaciónFuncional</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#Programming</a>

José A. AlonsoCan LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. <a href="https://arxiv.org/abs/2503.14183" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://arxiv.org/abs/2503.14183</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#Programming</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a>

Hacker NewsCoq-of-rust: Formal verification tool for Rust<a href="https://github.com/formal-land/coq-of-rust" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/formal-land/coq-of-rust</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/CoqOfRust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CoqOfRust</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalVerification</a> <a href="https://mastodon.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> <a href="https://mastodon.social/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Programming</a> <a href="https://mastodon.social/tags/Tools" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Tools</a>

José A. AlonsoReadings shared March 15, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/15-readings_shared_03-15-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/03/15-readings_shared_03-15-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="tag">#ACL2</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/CHR" class="mention hashtag" rel="tag">#CHR</a> <a href="https://mathstodon.xyz/tags/Constraint" class="mention hashtag" rel="tag">#Constraint</a> <a href="https://mathstodon.xyz/tags/Constraints" class="mention hashtag" rel="tag">#Constraints</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="tag">#Emacs</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#Logic</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="tag">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/NLP" class="mention hashtag" rel="tag">#NLP</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#Prolog</a>

José A. AlonsoRevisiting an early critique of formal verification. ~ Lawrence Paulson. <a href="https://lawrencecpaulson.github.io/2025/03/14/revisiting_demillo.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://lawrencecpaulson.github.io/2025/03/14/revisiting_demillo.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="tag">#FormalVerification</a>

Recent searches

Search options

Administered by:

Server stats:

#formalverification