toad.social

Jan :rust: :ferris:<a href="https://kolektiva.social/@d10c4n3" class="u-url mention" rel="nofollow noopener" target="_blank">@d10c4n3</a> Yes, this is another issue with the current <a href="https://floss.social/tags/LLM" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLM</a> architecture: they can't learn or improve. It's one big monolith - not composed of smaller parts (that could individually be improved or composed with each other).There _are_ AI architectures that are _actually reliable_...<a href="https://floss.social/@janriemer/114454349034565839" rel="nofollow noopener" translate="no" target="_blank">https://floss.social/@janriemer/114454349034565839</a>...but our industry has decided to hyperfocus on bullshit machines.<a href="https://mastodon.online/@larsmb" class="u-url mention" rel="nofollow noopener" target="_blank">@larsmb</a> <a href="https://floss.social/tags/ArtificialIntelligence" class="mention hashtag" rel="nofollow noopener" target="_blank">#ArtificialIntelligence</a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" 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" 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" target="_blank">#Z3</a> <a href="https://floss.social/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#SMT</a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#ModelChecking</a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener" target="_blank">#Proof</a>

Jan :rust: :ferris:F* (fstar) Interactive Tutorial:<a href="https://fstar-lang.org/tutorial/" rel="nofollow noopener" 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" target="_blank">#Aeneas</a>... so I can ultimately formally verify my <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> crate (former attempts with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener" target="_blank">#Creusot</a> and <a href="https://floss.social/tags/Kani" class="mention hashtag" rel="nofollow noopener" target="_blank">#Kani</a> failed for me).Aeneas: <a href="https://github.com/AeneasVerif/aeneas" rel="nofollow noopener" 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" target="_blank">#FormalVerification</a> <a href="https://floss.social/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#RustLang</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" target="_blank">#Rust</a> focus more and more on facilitating <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> - it perfectly aligns with <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener" 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!)

Rob SisonThere'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:<a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener" translate="no" target="_blank">https://youtu.be/7wcFx6OTEL4</a><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener" target="_blank">#sel4summit</a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#seL4</a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#verification</a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener" target="_blank">#operatingsystems</a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener" target="_blank">#microkernel</a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#HOL4</a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#modelchecking</a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalmethods</a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalverification</a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formal_methods</a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formal_verification</a>

KensanNew article up on ACM on Ada/SPARK title "Co-Developing Programs and Their Proof of Correctness". PDF is also available for download.<a href="https://cacm.acm.org/magazines/2024/3/280078-co-developing-programs-and-their-proof-of-correctness/fulltext" rel="nofollow noopener" translate="no" target="_blank">https://cacm.acm.org/magazines/2024/3/280078-co-developing-programs-and-their-proof-of-correctness/fulltext</a><a href="https://mastodon.social/tags/ada" class="mention hashtag" rel="nofollow noopener" target="_blank">#ada</a> <a href="https://mastodon.social/tags/spark" class="mention hashtag" rel="nofollow noopener" target="_blank">#spark</a> <a href="https://mastodon.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalverification</a>

Yaroslav KhnyginThis week I hosted a monthly meetup of Lisp Ireland, where Rafael Sadykov presented his talk "Lisp & Hardware Verification with ACL2".ACL2 is a theorem prover implemented in a subset of Common Lisp, and the talk discussed how it can be used for formal verification of various systems, and for hardware verification in particular.The recording was uploaded here: <a href="https://www.youtube.com/watch?v=iFEb9p54x_Q" rel="nofollow noopener" translate="no" target="_blank">https://www.youtube.com/watch?v=iFEb9p54x_Q</a><a href="https://mastodon.ie/tags/LispIreland" class="mention hashtag" rel="nofollow noopener" target="_blank">#LispIreland</a> <a href="https://mastodon.ie/tags/Meetup" class="mention hashtag" rel="nofollow noopener" target="_blank">#Meetup</a> <a href="https://mastodon.ie/tags/TechTalk" class="mention hashtag" rel="nofollow noopener" target="_blank">#TechTalk</a> <a href="https://mastodon.ie/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#Lisp</a> <a href="https://mastodon.ie/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#CommonLisp</a> <a href="https://mastodon.ie/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mastodon.ie/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://mastodon.ie/tags/HardwareVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#HardwareVerification</a> <a href="https://mastodon.ie/tags/Ireland" class="mention hashtag" rel="nofollow noopener" target="_blank">#Ireland</a>

José A. AlonsoThe importance of formal verification. <a href="https://formal.land/blog/2024/02/02/formal-verification-for-aleph-zero" rel="nofollow noopener" translate="no" target="_blank">https://formal.land/blog/2024/02/02/formal-verification-for-aleph-zero</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a>

José A. AlonsoGenerating and exploiting automated reasoning proof certificates. ~ Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar. <a href="https://cacm.acm.org/magazines/2023/10/276632-generating-and-exploiting-automated-reasoning-proof-certificates/abstract" rel="nofollow noopener" target="_blank">https://cacm.acm.org/magazines/2023/10/276632-generating-and-exploiting-automated-reasoning-proof-certificates/abstract</a> <a href="https://mathstodon.xyz/tags/AutomatedReasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#AutomatedReasoning</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a>

Frederic JacobsOne of the challenges with the deployment of more automated reasoning is often the tooling. Cool to see <a href="https://mastodon.social/tags/Cryspen" class="mention hashtag" rel="nofollow noopener" target="_blank">#Cryspen</a> invest in a new integrated development and verification environment based on hax. Congrats <a href="https://mastodon.social/@franziskus" class="u-url mention" rel="nofollow noopener" target="_blank">@franziskus</a> and team :) <a href="https://cryspen.com/post/cyber-campus-hax/" rel="nofollow noopener" translate="no" target="_blank">https://cryspen.com/post/cyber-campus-hax/</a><a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a>

Frederic JacobsGalois applied GPT-4 to generate a SAW memory safety proof for salsa20. Interesting example of what's currently possible at the intersection of LLMs and Formal Verification. Clearly more to come in that space. <a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://mastodon.social/tags/LLM" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLM</a> <a href="https://galois.com/blog/2023/08/applying-gpt-4-to-saw-formal-verification/" rel="nofollow noopener" translate="no" target="_blank">https://galois.com/blog/2023/08/applying-gpt-4-to-saw-formal-verification/</a>

FranziskusEnd of March I have been at the Real World Crypto Symposium to give a talk on the hacspec language, the hax tool, and the libcrux crypto library.Read more about it on Cryspen's blog.<a href="https://cryspen.com/post/rwc-2023/" rel="nofollow noopener" target="_blank">https://cryspen.com/post/rwc-2023/</a><a href="https://mastodon.social/tags/cryptography" class="mention hashtag" rel="nofollow noopener" target="_blank">#cryptography</a> <a href="https://mastodon.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalverification</a> <a href="https://mastodon.social/tags/tools" class="mention hashtag" rel="nofollow noopener" target="_blank">#tools</a> <a href="https://mastodon.social/tags/conference" class="mention hashtag" rel="nofollow noopener" target="_blank">#conference</a>

Daniel GrosseWoohoo! Our book, "Formal Verification of Structurally Complex Multipliers," has officially arrived in hardcover format! After putting in years of work, it's an indescribable feeling to finally have the physical copy in my hands.More information: <a href="https://link.springer.com/book/10.1007/978-3-031-24571-8" rel="nofollow noopener" target="_blank">https://link.springer.com/book/10.1007/978-3-031-24571-8</a><a href="https://fosstodon.org/tags/SymbolicComputerAlgebra" class="mention hashtag" rel="nofollow noopener" target="_blank">#SymbolicComputerAlgebra</a> <a href="https://fosstodon.org/tags/SCA" class="mention hashtag" rel="nofollow noopener" target="_blank">#SCA</a> <a href="https://fosstodon.org/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://fosstodon.org/tags/Circuits" class="mention hashtag" rel="nofollow noopener" target="_blank">#Circuits</a> <a href="https://fosstodon.org/tags/Hardware" class="mention hashtag" rel="nofollow noopener" target="_blank">#Hardware</a> <a href="https://fosstodon.org/tags/Springer" class="mention hashtag" rel="nofollow noopener" target="_blank">#Springer</a>

Frederic JacobsGluing together Hacspec, Jasmin and SSProve using Coq for end-to-end verification, from spec to implementation.It's great to see more integration efforts between formal verification stacks to improve confidence that implementations still satisfy all higher-level security properties.<a href="https://mastodon.social/tags/FV" class="mention hashtag" rel="nofollow noopener" target="_blank">#FV</a> <a href="https://mastodon.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://eprint.iacr.org/2023/185" rel="nofollow noopener" target="_blank">https://eprint.iacr.org/2023/185</a>

Steve EasterbrookA fuller <a href="https://fediscience.org/tags/introduction" class="mention hashtag" rel="nofollow noopener" target="_blank">#introduction</a>.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" target="_blank">#RequirementsEngineering</a>)This led me to explore socio-cognitive processes of large teams (<a href="https://fediscience.org/tags/DistributedCognition" class="mention hashtag" rel="nofollow noopener" target="_blank">#DistributedCognition</a>, <a href="https://fediscience.org/tags/STS" class="mention hashtag" rel="nofollow noopener" target="_blank">#STS</a>, <a href="https://fediscience.org/tags/Ethnography" class="mention hashtag" rel="nofollow noopener" target="_blank">#Ethnography</a>)I have worked for NASA studying software safety for spacecraft (<a href="https://fediscience.org/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a>, <a href="https://fediscience.org/tags/OrganizationalBehaviour" class="mention hashtag" rel="nofollow noopener" target="_blank">#OrganizationalBehaviour</a>)Now I study <a href="https://fediscience.org/tags/ClimateModels" class="mention hashtag" rel="nofollow noopener" target="_blank">#ClimateModels</a> + do <a href="https://fediscience.org/tags/ClimateData" class="mention hashtag" rel="nofollow noopener" target="_blank">#ClimateData</a> analytics, using all the above, plus <a href="https://fediscience.org/tags/SystemsThinking" class="mention hashtag" rel="nofollow noopener" target="_blank">#SystemsThinking</a>, <a href="https://fediscience.org/tags/DataScience" class="mention hashtag" rel="nofollow noopener" target="_blank">#DataScience</a>, & <a href="https://fediscience.org/tags/ML" class="mention hashtag" rel="nofollow noopener" target="_blank">#ML</a>

theruran 💻 🌐 :cereal_killer:worth posting this again, for those programmers who are having wicked thoughts of writing security-critical software in C or C++Source: "Exploitation in the era of <a href="https://hackers.town/tags/formalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalVerification</a>: A peek at a new frontier with <a href="https://hackers.town/tags/Ada" class="mention hashtag" rel="nofollow noopener" target="_blank">#Ada</a> / <a href="https://hackers.town/tags/SPARK" class="mention hashtag" rel="nofollow noopener" target="_blank">#SPARK</a>" by Adam Zabrocki and Alex Tereshkin, <a href="https://hackers.town/tags/DEFCON30" class="mention hashtag" rel="nofollow noopener" target="_blank">#DEFCON30</a>, 2022<a href="https://hackers.town/tags/infosec" class="mention hashtag" rel="nofollow noopener" target="_blank">#infosec</a> <a href="https://hackers.town/tags/DEFCON" class="mention hashtag" rel="nofollow noopener" target="_blank">#DEFCON</a>

Recent searches

Search options

Administered by:

Server stats:

#formalverification