给软件开发者准备的优质简报，每日阅读 10分钟。
Bill C-22, the Lawful Access Act: Dangerous backdoor surveillance risks remain
加拿大C-22法案：无令状访问调整但后门监控风险仍存
- 法案取消了C-2边境法案中广泛的无令状信息索取权，改为仅允许执法部门要求电信运营商确认特定个人是否为其客户
- 获取更多用户信息需经法官批准的生产令，但采用较低的“合理怀疑”标准仍存宪法争议
- 法案第二部分（SAAIA）要求电子服务提供商（包括互联网平台）配合执法测试监控能力并保密相关要求
- 新增元数据保留条款，强制核心提供商保留传输数据等非内容元数据最长一年
- 系统性漏洞例外条款被批评不足，可能降低网络安全性并涉及跨境数据共享，引发严重隐私担忧
Why I love FreeBSD
我为何热爱FreeBSD
- 作者在2002年首次接触FreeBSD手册时，被其完整、准确且持续更新的文档质量所震撼，这与他在Linux系统中常遇到的不完整或过时文档形成鲜明对比
- FreeBSD在相同硬件上的性能表现优于Linux，系统运行更稳定，编译时资源管理更优雅，不会出现过热或意外崩溃，且桌面体验更流畅无卡顿
- 系统的设计哲学强调“进化而非革命”，基础工具二十多年来保持兼容，确保生产环境的稳定性和可预测性，同时支持安全可逆的升级和原生功能如ZFS、bhyve虚拟化
- FreeBSD社区由真正热爱技术、具备专业能力和热情的人组成，包括开发者、基金会成员以及企业工程师，社区氛围积极且专注，不同于追逐短期商业利益的其他技术圈子
- 系统核心目标是高效、可靠地服务，不盲目追求潮流，注重实用性和一致性，其原生机制（如jails隔离）无需外部依赖即可管理，简化了运维并保障了数据安全
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
Leanstral：首个专为Lean 4设计的开源可信代码生成与验证模型
- Leanstral是首个专为Lean 4设计的开源代码代理模型，旨在生成代码并形式化验证其实现，适用于高风险领域如前沿数学研究和关键任务软件
- 模型采用高效稀疏架构，仅含60亿活跃参数，以Apache 2.0许可证开源权重，并通过Mistral Vibe、免费API端点及本地部署提供访问
- 在FLTEval评估中，Leanstral以单次推理显著超越更大规模的开源模型（如GLM5-744B和Kimi-K2.5-1T），并在多次推理中线性扩展性能至更高分数
- 相比Claude系列，Leanstral以极低成本实现竞争性性能：例如仅需36美元（pass@2）即达到26.3分，而Claude Sonnet需549美元仅得23.7分
- 实际应用案例证明，Leanstral能诊断Lean版本升级中的编译问题（如识别定义别名导致的模式匹配失败）并成功转换其他语言代码为Lean格式及证明程序属性
- 模型支持通过MCP（如lean-lsp-mcp）进行功能扩展，并集成于Mistral Vibe中供用户零配置使用
Kagi Small Web
Kagi Small Web：个性化小众网络内容探索平台
- 致力于推广“小众网络”（small web），强调展示真实个人发布的原创内容，以增强网络的人性化体验
- 提供多种内容浏览模式，包括“已点赞”、“视频”、“代码”和“漫画”等分类，方便用户按兴趣探索
- 内容分为三大主题板块：科技与科学、文化与创意、生活与世界，覆盖从人工智能到社会议题等多个细分领域
- 所有内容来源均基于开源列表，用户可访问 GitHub 确认是否被收录
- 仅显示最近七天内的更新，通过“下一篇”功能持续推送新鲜内容，并支持 RSS 订阅个性化内容流