lysdexic@programming.devEnglish · 21 天前The changing role of finite-state model checkingplus-squareahelwer.caexternal-linkmessage-square0linkfedilinkarrow-up14arrow-down10
arrow-up14arrow-down1external-linkThe changing role of finite-state model checkingplus-squareahelwer.calysdexic@programming.devEnglish · 21 天前message-square0linkfedilink
armchair_progamer@programming.dev · 1 年前My first verified (imperative) program [Lean]plus-squaremarkushimmel.deexternal-linkmessage-square0linkfedilinkarrow-up11arrow-down10
arrow-up11arrow-down1external-linkMy first verified (imperative) program [Lean]plus-squaremarkushimmel.dearmchair_progamer@programming.dev · 1 年前message-square0linkfedilink
cyph3rPunk@infosec.pub · 2 年前Verified Effectful Programming in F* - Catalin Hritcuplus-squareyoutu.beexternal-linkmessage-square0linkfedilinkarrow-up16arrow-down10
arrow-up16arrow-down1external-linkVerified Effectful Programming in F* - Catalin Hritcuplus-squareyoutu.becyph3rPunk@infosec.pub · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Linearizability! Refinement! Prophecy! (proving code correctness)plus-squaresurfingcomplexity.blogexternal-linkmessage-square0linkfedilinkarrow-up16arrow-down10
arrow-up16arrow-down1external-linkLinearizability! Refinement! Prophecy! (proving code correctness)plus-squaresurfingcomplexity.blogarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前The Hitchhiker’s Guide to Logical Verification (book)plus-squarebrowncs1951x.github.ioexternal-linkmessage-square1linkfedilinkarrow-up19arrow-down11
arrow-up18arrow-down1external-linkThe Hitchhiker’s Guide to Logical Verification (book)plus-squarebrowncs1951x.github.ioarmchair_progamer@programming.dev · 2 年前message-square1linkfedilink
armchair_progamer@programming.dev · 2 年前A curated list of awesome Rust checkersplus-squareburtonqin.github.ioexternal-linkmessage-square2linkfedilinkarrow-up117arrow-down11
arrow-up116arrow-down1external-linkA curated list of awesome Rust checkersplus-squareburtonqin.github.ioarmchair_progamer@programming.dev · 2 年前message-square2linkfedilink
armchair_progamer@programming.dev · 2 年前Modeling B-trees in TLA+plus-squaresurfingcomplexity.blogexternal-linkmessage-square0linkfedilinkarrow-up19arrow-down10
arrow-up19arrow-down1external-linkModeling B-trees in TLA+plus-squaresurfingcomplexity.blogarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Nondeterminism in Formal Specificationplus-squarebuttondown.emailexternal-linkmessage-square0linkfedilinkarrow-up111arrow-down10
arrow-up111arrow-down1external-linkNondeterminism in Formal Specificationplus-squarebuttondown.emailarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Diffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioexternal-linkmessage-square0linkfedilinkarrow-up17arrow-down10
arrow-up17arrow-down1external-linkDiffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Some notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgexternal-linkmessage-square1linkfedilinkarrow-up18arrow-down10
arrow-up18arrow-down1external-linkSome notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgarmchair_progamer@programming.dev · 2 年前message-square1linkfedilink
armchair_progamer@programming.dev · 2 年前coq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comexternal-linkmessage-square0linkfedilinkarrow-up16arrow-down10
arrow-up16arrow-down1external-linkcoq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Agda Core: The Dream and the Realityplus-squarejesper.cxexternal-linkmessage-square0linkfedilinkarrow-up111arrow-down10
arrow-up111arrow-down1external-linkAgda Core: The Dream and the Realityplus-squarejesper.cxarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Dafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.scienceexternal-linkmessage-square0linkfedilinkarrow-up15arrow-down11
arrow-up14arrow-down1external-linkDafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.sciencearmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Verus: Verified Rust for low-level systems codeplus-squaregithub.comexternal-linkmessage-square1linkfedilinkarrow-up119arrow-down10
arrow-up119arrow-down1external-linkVerus: Verified Rust for low-level systems codeplus-squaregithub.comarmchair_progamer@programming.dev · 2 年前message-square1linkfedilink
armchair_progamer@programming.dev · 2 年前Narya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comexternal-linkmessage-square0linkfedilinkarrow-up19arrow-down10
arrow-up19arrow-down1external-linkNarya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
armchair_progamer@programming.dev · 2 年前Don't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comexternal-linkmessage-square0linkfedilinkarrow-up110arrow-down10
arrow-up110arrow-down1external-linkDon't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comarmchair_progamer@programming.dev · 2 年前message-square0linkfedilink
demesisx@infosec.pubdeleted by creatorEnglish · 3 年前Verifiable Random Functionsplus-squareyoutu.beexternal-linkmessage-square0linkfedilinkarrow-up111arrow-down10
arrow-up111arrow-down1external-linkVerifiable Random Functionsplus-squareyoutu.bedemesisx@infosec.pubdeleted by creatorEnglish · 3 年前message-square0linkfedilink
armchair_progamer@programming.dev · 3 年前I formally modeled Dreidel for no good reasonplus-squarebuttondown.emailexternal-linkmessage-square1linkfedilinkarrow-up121arrow-down12
arrow-up119arrow-down1external-linkI formally modeled Dreidel for no good reasonplus-squarebuttondown.emailarmchair_progamer@programming.dev · 3 年前message-square1linkfedilink
armchair_progamer@programming.dev · 3 年前TLA+ in Isabelle/HOLplus-squaredavecturner.github.ioexternal-linkmessage-square0linkfedilinkarrow-up19arrow-down10
arrow-up19arrow-down1external-linkTLA+ in Isabelle/HOLplus-squaredavecturner.github.ioarmchair_progamer@programming.dev · 3 年前message-square0linkfedilink
armchair_progamer@programming.dev · 3 年前rzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioexternal-linkmessage-square0linkfedilinkarrow-up17arrow-down10
arrow-up17arrow-down1external-linkrzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioarmchair_progamer@programming.dev · 3 年前message-square0linkfedilink
