Proofcraft 新闻 - 2024 - SegmentFault 思否

Proofcraft's Holiday Greetings: Proofcraft sent out holiday greetings with a related image.
Part of DARPA's PROVERS Program:
- DARPA funds the PROVERS program to make formal methods accessible to non-experts.
- Proofcraft is in the successful INSPECTA team, led by Darren Cofer from Collins Aerospace with contributions from multiple institutions.
- Proofcraft will reduce reliance on experts for seL4 formal proofs in 3 ways: automated platform port verification, architecture-split of proofs, and completing the MCS seL4 functional correctness proof.
Advocating Formal Methods:
- The White House's report prompted a seminar on Formal Specification and Validation at Scale.
- Proofcraft CEO June Andronick presented at the event along with other experts.
Impact at the 2024 seL4 Summit:
- Proofcraft was a sponsor and had a strong on-stage presence, delivering technical talks and participating in a panel.
- Michael McInerney presented seL4 verification status and plans.
- Corey Lewis shared the roadmap for a verified static multikernel configuration.
- All Summit sessions are available online.
Sponsoring seL4 Summit 2024: Proofcraft is sponsoring the 2024 seL4 summit in Sydney.
Sponsoring HCSS'24: Proofcraft is a sponsor of the 24th HCSS Conference in Annapolis.
June's Keynote at MatchPoints: June was a keynote speaker at MatchPoints in Denmark, presenting on seL4 and participating in a "Meet the Expert lunch".
seL4 on AArch64 Verified: Proofcraft completed the formal proof that seL4 on AArch64 behaves as specified, on par with other architectures.
Automated Proof Checks: Proofcraft extended seL4 proof checks to include other verification platforms and configurations, with more in progress.