det.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Mastodon Server des Unterhaltungsfernsehen Ehrenfeld zum dezentralen Diskurs.

Administered by:

Server stats:

1.8K
active users

#formalmethods

3 posts3 participants0 posts today
Alley Stoughton<p>Interested in theoretical cryptography and/or formal methods? Boston University is hosting a summer school on Universally Composable Security and the EasyUC framework for formalizing UC models and proofs.</p><p>The school is from August 11 - 14, 2025. Registration is free, and we're supporting both in person and Zoom participation.</p><p>For more information and to register, visit:</p><p><a href="https://www.bu.edu/riscs/events/uc-easyuc-summer-school/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">bu.edu/riscs/events/uc-easyuc-</span><span class="invisible">summer-school/</span></a></p><p><a href="https://fosstodon.org/tags/Cryptography" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Cryptography</span></a> <a href="https://fosstodon.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a></p>
Lobsters<p>Kiro and the future of AI spec-driven software development <a href="https://lobste.rs/s/gcgqvb" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/gcgqvb</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/practices" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>practices</span></a> <a href="https://mastodon.social/tags/vibecoding" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>vibecoding</span></a><br><a href="https://kiro.dev/blog/kiro-and-the-future-of-software-development/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">kiro.dev/blog/kiro-and-the-fut</span><span class="invisible">ure-of-software-development/</span></a></p>
Dr. Anna Latour<p>I am hiring!</p><p>I have a fully funded PhD position available for someone with an interest in logic and statistics, at Delft University of Technology (Netherlands).</p><p>Application deadline: 31 August 2025</p><p><a href="https://careers.tudelft.nl/job/Delft-PhD-Position-Symbolic-AI-and-Reasoning-Under-Uncertainty-2628-CD/824585702/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">careers.tudelft.nl/job/Delft-P</span><span class="invisible">hD-Position-Symbolic-AI-and-Reasoning-Under-Uncertainty-2628-CD/824585702/</span></a></p><p><a href="https://mathstodon.xyz/tags/AcademicJobs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AcademicJobs</span></a> <a href="https://mathstodon.xyz/tags/AcademicMastodon" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AcademicMastodon</span></a> <a href="https://mathstodon.xyz/tags/GetFediHired" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>GetFediHired</span></a> <a href="https://mathstodon.xyz/tags/AcademicJob" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AcademicJob</span></a> <a href="https://mathstodon.xyz/tags/SymbolicAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SymbolicAI</span></a> <a href="https://mathstodon.xyz/tags/Statistics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Statistics</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/ConstraintProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ConstraintProgramming</span></a> <a href="https://mathstodon.xyz/tags/CombinatorialOptimisation" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CombinatorialOptimisation</span></a> <a href="https://mathstodon.xyz/tags/SensitivityAnalysis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SensitivityAnalysis</span></a> <a href="https://mathstodon.xyz/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a> <a href="https://mathstodon.xyz/tags/CombinatorialOptimization" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CombinatorialOptimization</span></a> <a href="https://mathstodon.xyz/tags/Delft" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Delft</span></a> <a href="https://mathstodon.xyz/tags/TUDelft" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TUDelft</span></a> <a href="https://mathstodon.xyz/tags/AcademicChatter" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AcademicChatter</span></a></p>
Lobsters<p>Concurrent Programming with Harmony <a href="https://lobste.rs/s/ljookn" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/ljookn</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/book" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>book</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a><br><a href="https://harmony.cs.cornell.edu/book/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">harmony.cs.cornell.edu/book/</span><span class="invisible"></span></a></p>
Jan :rust: :ferris:<p>ESBMC - An Efficient SMT-based Bounded Model Checker</p><p><a href="https://ssvlab.github.io/esbmc/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">ssvlab.github.io/esbmc/</span><span class="invisible"></span></a></p><p>"ESBMC is an open-source, [...], context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well."</p><p>1/3</p><p><a href="https://floss.social/tags/SMT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SMT</span></a> <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/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalMethods</span></a> <a href="https://floss.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ModelChecking</span></a></p>
Lobsters<p>Oregon Programming Languages Summer School (OPLSS) 2025: Types, Logic, and Formal Methods <a href="https://lobste.rs/s/cga7nb" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/cga7nb</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/video" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>video</span></a> <a href="https://mastodon.social/tags/education" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>education</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a><br><a href="https://www.cs.uoregon.edu/research/summerschool/summer25/topics.php" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">cs.uoregon.edu/research/summer</span><span class="invisible">school/summer25/topics.php</span></a></p>
Lobsters<p>Preventing Reentrancy Bugs From Creeping Back In: Linking TLA+ Models to Rust Code <a href="https://lobste.rs/s/8tmodh" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/8tmodh</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</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/testing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>testing</span></a><br><a href="https://medium.com/dfinity/preventing-reentrancy-bugs-from-creeping-back-in-linking-tla-models-to-rust-code-c7854eb9458d" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">medium.com/dfinity/preventing-</span><span class="invisible">reentrancy-bugs-from-creeping-back-in-linking-tla-models-to-rust-code-c7854eb9458d</span></a></p>
Lobsters<p>The Tree Borrows paper is finally published <a href="https://lobste.rs/s/baio5y" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/baio5y</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a> <a href="https://mastodon.social/tags/rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rust</span></a><br><a href="https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">ralfj.de/blog/2025/07/07/tree-</span><span class="invisible">borrows-paper.html</span></a></p>
Lobsters<p>“Bad Apple!!” But It’s 3288 Lean Tactics Spamming VSCode <a href="https://lobste.rs/s/ccvkpv" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/ccvkpv</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/graphics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>graphics</span></a><br><a href="https://unnamed.website/posts/bad-apple-lean-tactic/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">unnamed.website/posts/bad-appl</span><span class="invisible">e-lean-tactic/</span></a></p>
Lobsters<p>My first verified (imperative) program via <span class="h-card" translate="no"><a href="https://social.treehouse.systems/@RunxiYu" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>RunxiYu</span></a></span> <a href="https://lobste.rs/s/giycc1" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/giycc1</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a><br><a href="https://markushimmel.de/blog/my-first-verified-imperative-program/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">markushimmel.de/blog/my-first-</span><span class="invisible">verified-imperative-program/</span></a></p>
Lobsters<p>A supposedly worthwhile contract I'll never do again by <span class="h-card" translate="no"><a href="https://discuss.systems/@ahelwer" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>ahelwer</span></a></span> <a href="https://lobste.rs/s/zhiv3y" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/zhiv3y</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a><br><a href="https://ahelwer.ca/post/2025-07-04-tla-contracts/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ahelwer.ca/post/2025-07-04-tla</span><span class="invisible">-contracts/</span></a></p>
Lobsters<p>Inequality Union Finds: Baby Steps to Refinement E-graphs by <span class="h-card" translate="no"><a href="https://types.pl/@sandmouth" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>sandmouth</span></a></span> <a href="https://lobste.rs/s/wahapd" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/wahapd</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a><br><a href="https://www.philipzucker.com/le_find/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">philipzucker.com/le_find/</span><span class="invisible"></span></a></p>
Lobsters<p>Rapid Prototyping a Safe, Logless Reconfiguration Protocol for MongoDB with TLA+ <a href="https://lobste.rs/s/teixnn" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/teixnn</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/distributed" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>distributed</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a><br><a href="https://www.mongodb.com/blog/post/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">mongodb.com/blog/post/technica</span><span class="invisible">l/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus</span></a></p>
Lobsters<p>Proving that every program halts <a href="https://lobste.rs/s/l280ru" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/l280ru</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/satire" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>satire</span></a><br><a href="https://ntietz.com/blog/proving-that-every-program-halts/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ntietz.com/blog/proving-that-e</span><span class="invisible">very-program-halts/</span></a></p>
Lobsters<p>Telescopes Are Tries: A Dependent Type Shellac on SQLite by <span class="h-card" translate="no"><a href="https://types.pl/@sandmouth" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>sandmouth</span></a></span> <a href="https://lobste.rs/s/u6xhiw" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/u6xhiw</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/databases" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>databases</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a><br><a href="https://www.philipzucker.com/telescope_tries/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">philipzucker.com/telescope_tri</span><span class="invisible">es/</span></a></p>
Lobsters<p>StarMalloc: verified memory allocator <a href="https://lobste.rs/s/jpfyd6" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/jpfyd6</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>compsci</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>security</span></a><br><a href="https://dl.acm.org/doi/10.1145/3689773" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">dl.acm.org/doi/10.1145/3689773</span><span class="invisible"></span></a></p>
Lobsters<p>100 years of Zermelo’s axiom of choice: What was the problem with it? <a href="https://lobste.rs/s/kbcp5p" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/kbcp5p</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>math</span></a><br><a href="https://research.mietek.io/mi.MartinLof2006.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">research.mietek.io/mi.MartinLo</span><span class="invisible">f2006.html</span></a></p>
Lobsters<p>Writing a Verified Postfix Calculator in Ada/SPARK <a href="https://lobste.rs/s/uwhv3o" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/uwhv3o</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programming</span></a><br><a href="https://pyjarrett.github.io/2025/06/10/postfix-calculator.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">pyjarrett.github.io/2025/06/10</span><span class="invisible">/postfix-calculator.html</span></a></p>
Lobsters<p>Proving completeness of an eventually perfect failure detector in Lean4 <a href="https://lobste.rs/s/adl5af" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/adl5af</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/distributed" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>distributed</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a><br><a href="https://protocols-made-fun.com/lean/2025/06/10/lean-epfd-completeness.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">protocols-made-fun.com/lean/20</span><span class="invisible">25/06/10/lean-epfd-completeness.html</span></a></p>
Lobsters<p>Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library <a href="https://lobste.rs/s/p8uq6e" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">lobste.rs/s/p8uq6e</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/c" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>c</span></a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://mastodon.social/tags/rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rust</span></a><br><a href="https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">microsoft.com/en-us/research/b</span><span class="invisible">log/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/</span></a></p>