Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
c.im is one of the many independent Mastodon servers you can use to participate in the fediverse.
C.IM is a general, mainly English-speaking Mastodon instance.

Administered by:

Server stats:

2.8K
active users

c.im: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#formalverification

4 posts4 participants1 post today
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>
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>
Hacker News<p>Coq-of-rust: Formal verification tool for Rust</p><p><a href="https://github.com/formal-land/coq-of-rust" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/formal-land/coq-of-</span><span class="invisible">rust</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/CoqOfRust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CoqOfRust</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/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> <a href="https://mastodon.social/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mastodon.social/tags/Tools" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Tools</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>
LavX News<p>AI and the Future of Mathematical Proofs: A New Era of Collaboration and Innovation</p><p>As AI continues to evolve, the intersection of mathematics and machine learning is poised to revolutionize how proofs are generated and verified. With the advent of interactive theorem provers and adv...</p><p><a href="https://news.lavx.hu/article/ai-and-the-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">news.lavx.hu/article/ai-and-th</span><span class="invisible">e-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation</span></a></p><p><a href="https://mastodon.cloud/tags/news" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>news</span></a> <a href="https://mastodon.cloud/tags/tech" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>tech</span></a> <a href="https://mastodon.cloud/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mastodon.cloud/tags/InteractiveTheoremProvers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>InteractiveTheoremProvers</span></a> <a href="https://mastodon.cloud/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AlphaProof</span></a></p>
Science News<p>20.01.25: A milestone for IT security: Contract by @CybAgBund with 5 partners for the "Trustworthy IT Ecosystem" (ÖvIT) research program. <br>Aim: Proven IT security and a global network of experts.<br><a href="https://idw-online.social/tags/%C3%96vIT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ÖvIT</span></a> <a href="https://idw-online.social/tags/Cybersecurity" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Cybersecurity</span></a> <a href="https://idw-online.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://idw-online.social/tags/Innovation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Innovation</span></a><br><a href="https://nachrichten.idw-online.de/2025/01/20/cyberagentur-signs-five-contracts-for-the-verifiably-secure-it-ecosystem-research-program" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">nachrichten.idw-online.de/2025</span><span class="invisible">/01/20/cyberagentur-signs-five-contracts-for-the-verifiably-secure-it-ecosystem-research-program</span></a></p>
LavX News<p>Genefication: The Future of Code Generation Meets Formal Verification</p><p>In a world where generative AI is revolutionizing software development, the challenge of ensuring the correctness of AI-generated code looms large. Enter Genefication, a groundbreaking approach that m...</p><p><a href="https://news.lavx.hu/article/genefication-the-future-of-code-generation-meets-formal-verification" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">news.lavx.hu/article/geneficat</span><span class="invisible">ion-the-future-of-code-generation-meets-formal-verification</span></a></p><p><a href="https://mastodon.cloud/tags/news" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>news</span></a> <a href="https://mastodon.cloud/tags/tech" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>tech</span></a> <a href="https://mastodon.cloud/tags/Genefication" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Genefication</span></a> <a href="https://mastodon.cloud/tags/TLA" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TLA</span></a>+ <a href="https://mastodon.cloud/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>
ExploreLive feeds
About