Jan :rust: :ferris:<p>Hm...I'm running into a timeout with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Creusot</span></a> when trying to verify a simple `add` operation on a HashMap newtype 🤔 </p><p><a href="https://github.com/creusot-rs/creusot/discussions/1477" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/creusot-rs/creusot/</span><span class="invisible">discussions/1477</span></a></p><p>Does anyone have any idea what's going on here?</p><p>Disclaimer: I'm totally new to creusot and <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a>, so please be gentle with me.😊 </p><p>Boosts very much appreciated. :boost_love: </p><p>Thank you! ❤️ </p><p><a href="https://floss.social/tags/IDontKnowWhatIamDoing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IDontKnowWhatIamDoing</span></a> <a href="https://floss.social/tags/Help" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Help</span></a> <a href="https://floss.social/tags/FediHelp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FediHelp</span></a> <a href="https://floss.social/tags/FollowerPower" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FollowerPower</span></a> <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RustLang</span></a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Proof</span></a> <a href="https://floss.social/tags/Timeout" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Timeout</span></a></p>
Recent searches
No recent searches
Search options
Only available when logged in.
veganism.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Veganism Social is a welcoming space on the internet for vegans to connect and engage with the broader decentralized social media community.
Administered by:
Server stats:
134active users
veganism.social: About · Status · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.3.7+vegan
#formalverification
2 posts · 1 participant · 0 posts today
Jan :rust: :ferris:<p>creuSAT - A formally verified <a href="https://floss.social/tags/SAT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SAT</span></a> solver written in <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> and verified with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Creusot</span></a>.</p><p><a href="https://github.com/sarsko/CreuSAT" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/sarsko/CreuSAT</span><span class="invisible"></span></a></p><p>Mindblowing! 🤯 </p><p><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RustLang</span></a></p>
Jan :rust: :ferris:<p>Iris Project | A Higher-Order Concurrent Separation Logic Framework,<br>implemented and verified in the Rocq Prover</p><p><a href="https://iris-project.org/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">iris-project.org/</span><span class="invisible"></span></a></p><p><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/Iris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Iris</span></a> <a href="https://floss.social/tags/ConcurrentSeparationLogic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ConcurrentSeparationLogic</span></a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Proof</span></a></p>
N-gated Hacker News<p>🧙♂️✨ Ah, the mystical realm of ZK circuits now has its own shiny <a href="https://mastodon.social/tags/DSL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DSL</span></a> in Lean4! Because nothing screams "fun and approachable" like embedding formal verification into an already niche <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programming</span></a> language. 🤖🔧 By the time you've deciphered this, you'll wish you had zero knowledge of Clean.<br><a href="https://blog.zksecurity.xyz/posts/clean/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">blog.zksecurity.xyz/posts/clea</span><span class="invisible">n/</span></a> <a href="https://mastodon.social/tags/ZKcircuits" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ZKcircuits</span></a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mastodon.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://mastodon.social/tags/fun" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>fun</span></a> <a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HackerNews</span></a> <a href="https://mastodon.social/tags/ngated" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ngated</span></a></p>
Cryspen<p>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! 🔒</p><p><a href="https://cryspen.com/post/control-flow-analysis/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cryspen.com/post/control-flow-</span><span class="invisible">analysis/</span></a></p><p><a href="https://ioc.exchange/tags/rustlang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rustlang</span></a> <a href="https://ioc.exchange/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://ioc.exchange/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>security</span></a></p>
N-gated Hacker News<p>🤖✨ Oh, joy! Another attempt at taming the chaotic beast that is machine learning by shoving it into the box of 'formal verification' using Lean 4. Because clearly, <a href="https://mastodon.social/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> needs even more cumbersome frameworks to prove it's not a total mess! 🙃🔧<br><a href="https://github.com/fraware/leanverifier" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/fraware/leanverifier</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/machinelearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>machinelearning</span></a> <a href="https://mastodon.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mastodon.social/tags/chaos" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>chaos</span></a> <a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HackerNews</span></a> <a href="https://mastodon.social/tags/ngated" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ngated</span></a></p>
Hacker News<p>Formal Verification for Machine Learning Models Using Lean 4</p><p><a href="https://github.com/fraware/leanverifier" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/fraware/leanverifier</span><span class="invisible"></span></a></p><p><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HackerNews</span></a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mastodon.social/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>MachineLearning</span></a> <a href="https://mastodon.social/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mastodon.social/tags/AIResearch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AIResearch</span></a> <a href="https://mastodon.social/tags/TechInnovation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TechInnovation</span></a></p>
José A. Alonso<p>Readings shared March 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/19-readings_shared_03-19-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/19-readings_shared_03-19-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CompSci</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programaci%C3%B3nFuncional" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgramaciónFuncional</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a></p>
José A. Alonso<p>Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. <a href="https://arxiv.org/abs/2503.14183" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.14183</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
José A. Alonso<p>Readings shared March 15, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/15-readings_shared_03-15-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/15-readings_shared_03-15-25</span></a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ACL2</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/CHR" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CHR</span></a> <a href="https://mathstodon.xyz/tags/Constraint" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Constraint</span></a> <a href="https://mathstodon.xyz/tags/Constraints" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Constraints</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>MachineLearning</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/NLP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>NLP</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Prolog</span></a></p>
José A. Alonso<p>Revisiting an early critique of formal verification. ~ Lawrence Paulson. <a href="https://lawrencecpaulson.github.io/2025/03/14/revisiting_demillo.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">lawrencecpaulson.github.io/202</span><span class="invisible">5/03/14/revisiting_demillo.html</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
José A. Alonso<p>Readings shared March 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/11-readings_shared_03-11-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/11-readings_shared_03-11-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Jape" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Jape</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/MAS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>MAS</span></a> <a href="https://mathstodon.xyz/tags/Mace" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Mace</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Otter" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Otter</span></a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PVS</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/SMLs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SMLs</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Scala" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Scala</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Can proof assistants verify multi-agent systems? ~ Julian Alfredo Mendez, Timotheus Kampik. <a href="https://arxiv.org/abs/2503.06812" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.06812</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/MAS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>MAS</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Scala" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Scala</span></a></p>
José A. Alonso<p>Readings shared November 29, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/11/29-readings_shared_11-29-24" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/11/29-readings_shared_11-29-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Calculemus</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>MachineLearning</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/AIMO" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AIMO</span></a> <a href="https://mathstodon.xyz/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AlphaProof</span></a> <a href="https://mathstodon.xyz/tags/AlphaGeometry" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AlphaGeometry</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/Dafny" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Dafny</span></a></p>
José A. Alonso<p>dafny-annotator: AI-assisted verification of Dafny programs. ~ Gabriel Poesia, Chloe Loughridge, Nada Amin. <a href="https://arxiv.org/abs/2411.15143" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2411.15143</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Dafny" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Dafny</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
José A. Alonso<p>Effectiveness of Large Language Models to generate formally verified C code. ~ Merlijn Sevenhuijsen. <a href="https://www.diva-portal.org/smash/get/diva2:1915138/FULLTEXT02" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">diva-portal.org/smash/get/diva</span><span class="invisible">2:1915138/FULLTEXT02</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_verification</span></a></p>
Steve Easterbrook<p>A fuller <a href="https://fediscience.org/tags/introduction" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>introduction</span></a>.</p><p>My PhD was in software systems analysis: how to handle poorly understood, conflicting system requirements (<a href="https://fediscience.org/tags/RequirementsEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RequirementsEngineering</span></a>)</p><p>This led me to explore socio-cognitive processes of large teams (<a href="https://fediscience.org/tags/DistributedCognition" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DistributedCognition</span></a>, <a href="https://fediscience.org/tags/STS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>STS</span></a>, <a href="https://fediscience.org/tags/Ethnography" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ethnography</span></a>)</p><p>I have worked for NASA studying software safety for spacecraft (<a href="https://fediscience.org/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a>, <a href="https://fediscience.org/tags/OrganizationalBehaviour" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>OrganizationalBehaviour</span></a>)</p><p>Now I study <a href="https://fediscience.org/tags/ClimateModels" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateModels</span></a> + do <a href="https://fediscience.org/tags/ClimateData" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateData</span></a> analytics, using all the above, plus <a href="https://fediscience.org/tags/SystemsThinking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SystemsThinking</span></a>, <a href="https://fediscience.org/tags/DataScience" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DataScience</span></a>, & <a href="https://fediscience.org/tags/ML" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ML</span></a></p>
theruran 💻 🌐 :cereal_killer:<p>worth posting this again, for those programmers who are having wicked thoughts of writing security-critical software in C or C++</p><p>Source: "Exploitation in the era of <a href="https://hackers.town/tags/formalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalVerification</span></a>: A peek at a new frontier with <a href="https://hackers.town/tags/Ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ada</span></a> / <a href="https://hackers.town/tags/SPARK" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SPARK</span></a>" by Adam Zabrocki and Alex Tereshkin, <a href="https://hackers.town/tags/DEFCON30" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON30</span></a>, 2022</p><p><a href="https://hackers.town/tags/infosec" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>infosec</span></a> <a href="https://hackers.town/tags/DEFCON" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON</span></a></p>
VegansExploreLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload